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