let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)
let X, Y, Z be ManySortedSet of I; :: 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 Th39
.= ((X /\ Y) \/ ((Y /\ Z) \/ Z)) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X) by Th34
.= ((X /\ Y) \/ Z) /\ (((X /\ Y) \/ (Y /\ Z)) \/ X) by Th37
.= ((X /\ Y) \/ Z) /\ (((X /\ Y) \/ X) \/ (Y /\ Z)) by Th34
.= ((X /\ Y) \/ Z) /\ (X \/ (Y /\ Z)) by Th37
.= ((X \/ Z) /\ (Y \/ Z)) /\ (X \/ (Y /\ Z)) by Th39
.= ((X \/ Z) /\ (Y \/ Z)) /\ ((X \/ Y) /\ (X \/ Z)) by Th39
.= (X \/ Y) /\ (((Y \/ Z) /\ (X \/ Z)) /\ (X \/ Z)) by Th35
.= (X \/ Y) /\ ((Y \/ Z) /\ ((X \/ Z) /\ (X \/ Z))) by Th35
.= ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X) by Th35 ; :: thesis: verum