let I be set ; :: thesis: for X, Z, Y being ManySortedSet of I st X c= Z holds
X \/ (Y /\ Z) = (X \/ Y) /\ Z
let X, Z, Y be ManySortedSet of I; :: thesis: ( X c= Z implies X \/ (Y /\ Z) = (X \/ Y) /\ Z )
assume A1: X c= Z ; :: thesis: X \/ (Y /\ Z) = (X \/ Y) /\ Z

now

let i be set ; :: thesis: ( i in I implies (X \/ (Y /\ Z)) . i = ((X \/ Y) /\ Z) . i )
assume A2: i in I ; :: thesis: (X \/ (Y /\ Z)) . i = ((X \/ Y) /\ Z) . i
then A3: X . i c= Z . i by A1, Def5;
thus (X \/ (Y /\ Z)) . i = (X . i) \/ ((Y /\ Z) . i) by A2, Def7
.= (X . i) \/ ((Y . i) /\ (Z . i)) by A2, Def8
.= ((X . i) \/ (Y . i)) /\ (Z . i) by A3, XBOOLE_1:30
.= ((X \/ Y) . i) /\ (Z . i) by A2, Def7
.= ((X \/ Y) /\ Z) . i by A2, Def8 ; :: thesis: verum

end;

hence X \/ (Y /\ Z) = (X \/ Y) /\ Z by Th3; :: thesis: verum