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
let i be set ; :: according to PBOOLE:def 10 :: 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, Def2;
thus (X \/ (Y /\ Z)) . i = (X . i) \/ ((Y /\ Z) . i) by A2, Def4
.= (X . i) \/ ((Y . i) /\ (Z . i)) by A2, Def5
.= ((X . i) \/ (Y . i)) /\ (Z . i) by A3, XBOOLE_1:30
.= ((X \/ Y) . i) /\ (Z . i) by A2, Def4
.= ((X \/ Y) /\ Z) . i by A2, Def5 ; :: thesis: verum