let X, Y, Z be set ; :: thesis: ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)
thus ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = (((X /\ Y) \/ (Y /\ Z)) \/ Z) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X) by Th24
.= ((X /\ Y) \/ ((Y /\ Z) \/ Z)) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X) by Th4
.= ((X /\ Y) \/ Z) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X) by Th22
.= ((X /\ Y) \/ Z) /\ (((X /\ Y) \/ X) \/ (Y /\ Z)) by Th4
.= ((X /\ Y) \/ Z) /\ (X \/ (Y /\ Z)) by Th22
.= ((X \/ Z) /\ (Y \/ Z)) /\ (X \/ (Y /\ Z)) by Th24
.= ((X \/ Z) /\ (Y \/ Z)) /\ ((X \/ Y) /\ (X \/ Z)) by Th24
.= (X \/ Y) /\ (((Y \/ Z) /\ (X \/ Z)) /\ (X \/ Z)) by Th16
.= (X \/ Y) /\ ((Y \/ Z) /\ ((X \/ Z) /\ (X \/ Z))) by Th16
.= ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X) by Th16 ; :: thesis: verum