let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Z holds
X (\/) (Y (/\) Z) = (X (\/) Y) (/\) Z
let X, Y, Z 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 object ; :: 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;
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