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