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