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