let X, Y, Z be set ; :: thesis: (X /\ Z) \+\ (Y /\ Z) = (X \+\ Y) /\ Z
thus (X /\ Z) \+\ (Y /\ Z) = ((X \ Y) /\ Z) \/ ((Y /\ Z) \ (X /\ Z)) by Th111
.= ((X \ Y) /\ Z) \/ ((Y \ X) /\ Z) by Th111
.= (X \+\ Y) /\ Z by Th23 ; :: thesis: verum