% Selfdual version of the distributive law:

(all x all y all z
subclass(intersection(union(x,y),z),union(x,intersection(y,z)))).