let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds
( (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z) & X \/ (Y \/ Z) = (X \/ Y) \/ (X \/ Z) )
let X, Y, Z be ManySortedSet of I; :: thesis: ( (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z) & X \/ (Y \/ Z) = (X \/ Y) \/ (X \/ Z) )
thus (X \/ Y) \/ Z = X \/ (Y \/ (Z \/ Z)) by Th34
.= X \/ ((Z \/ Y) \/ Z) by Th34
.= (X \/ Z) \/ (Y \/ Z) by Th34 ; :: thesis: X \/ (Y \/ Z) = (X \/ Y) \/ (X \/ Z)
thus X \/ (Y \/ Z) = (X \/ X) \/ (Y \/ Z)
.= X \/ (X \/ (Y \/ Z)) by Th34
.= X \/ ((X \/ Y) \/ Z) by Th34
.= (X \/ Y) \/ (X \/ Z) by Th34 ; :: thesis: verum