let X, Y, Z be set ; :: thesis: X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
A1: X /\ Y c= X by Th17;
(X /\ Y) \ (X /\ Z) = ((X /\ Y) \ X) \/ ((X /\ Y) \ Z) by Lm2
.= {} \/ ((X /\ Y) \ Z) by A1, Lm1
.= (X /\ Y) \ Z ;
hence X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z) by Th49; :: thesis: verum