formula_list(usable). % almost the distributive law of intersection over union

	( all x y z ( n(z,y) = Z -> n(u(x,y),z) = n(z,x) )). % 25

end_of_list.