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