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