let X, Y, Z be set ; :: thesis: (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
set S1 = X \ (Y \/ Z);
set S2 = Y \ (X \/ Z);
set S3 = Z \ (X \/ Y);
set S4 = (X /\ Y) /\ Z;
thus (X \+\ Y) \+\ Z = (((X \ Y) \ Z) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th42
.= ((X \ (Y \/ Z)) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th41
.= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th41
.= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ (Z \ ((X \/ Y) \ (X /\ Y))) by Th55
.= ((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ (((X /\ Y) /\ Z) \/ (Z \ (X \/ Y))) by Th52
.= (((X \ (Y \/ Z)) \/ (Y \ (X \/ Z))) \/ ((X /\ Y) /\ Z)) \/ (Z \ (X \/ Y)) by Th4
.= (((X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)) \/ (Y \ (X \/ Z))) \/ (Z \ (X \/ Y)) by Th4
.= ((X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)) \/ ((Y \ (X \/ Z)) \/ (Z \ (X \/ Y))) by Th4
.= ((X \ (Y \/ Z)) \/ (X /\ (Y /\ Z))) \/ ((Y \ (X \/ Z)) \/ (Z \ (X \/ Y))) by Th16
.= (X \ ((Y \/ Z) \ (Y /\ Z))) \/ ((Y \ (X \/ Z)) \/ (Z \ (X \/ Y))) by Th52
.= (X \ ((Y \ Z) \/ (Z \ Y))) \/ ((Y \ (X \/ Z)) \/ (Z \ (Y \/ X))) by Th55
.= (X \ ((Y \ Z) \/ (Z \ Y))) \/ ((Y \ (Z \/ X)) \/ ((Z \ Y) \ X)) by Th41
.= (X \ ((Y \ Z) \/ (Z \ Y))) \/ (((Y \ Z) \ X) \/ ((Z \ Y) \ X)) by Th41
.= X \+\ (Y \+\ Z) by Th42 ; :: thesis: verum