let I be set ; :: thesis: for A, X being ManySortedSet of I
for B being non-empty ManySortedSet of I st X c= union (A (\/) B) & ( for Y being ManySortedSet of I st Y in B holds
Y (/\) X = EmptyMS I ) holds
X c= union A
let A, X be ManySortedSet of I; :: thesis: for B being non-empty ManySortedSet of I st X c= union (A (\/) B) & ( for Y being ManySortedSet of I st Y in B holds
Y (/\) X = EmptyMS I ) holds
X c= union A
let B be non-empty ManySortedSet of I; :: thesis: ( X c= union (A (\/) B) & ( for Y being ManySortedSet of I st Y in B holds
Y (/\) X = EmptyMS I ) implies X c= union A )
assume that
A1: X c= union (A (\/) B) and
A2: for Y being ManySortedSet of I st Y in B holds
Y (/\) X = EmptyMS I ; :: thesis: X c= union A
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or X . i c= (union A) . i )
assume A3: i in I ; :: thesis: X . i c= (union A) . i
A4: for Y9 being set st Y9 in B . i holds
Y9 misses X . i

proof

consider M being ManySortedSet of I such that
A5: M in B by PBOOLE:134;
let Y9 be set ; :: thesis: ( Y9 in B . i implies Y9 misses X . i )
assume A6: Y9 in B . i ; :: thesis: Y9 misses X . i
dom (M +* (i .--> Y9)) = I by A3, Lm1;
then reconsider K = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A7: dom (i .--> Y9) = {i} ;
i in {i} by TARSKI:def 1;
then A8: K . i = (i .--> Y9) . i by A7, FUNCT_4:13
.= Y9 by FUNCOP_1:72 ;
K in B

proof

let j be object ; :: according to PBOOLE:def 1 :: thesis: ( not j in I or K . j in B . j )
assume A9: j in I ; :: thesis: K . j in B . j

now :: thesis: ( ( j = i & K . j in B . j ) or ( j <> i & K . j in B . j ) )

per cases ( j = i or j <> i ) ;

case j = i ; :: thesis: K . j in B . j

hence K . j in B . j by A6, A8; :: thesis: verum

end;

case j <> i ; :: thesis: K . j in B . j

then not j in dom (i .--> Y9) by TARSKI:def 1;
then K . j = M . j by FUNCT_4:11;
hence K . j in B . j by A5, A9; :: thesis: verum

end;

end;

end;

hence K . j in B . j ; :: thesis: verum

end;

then K (/\) X = EmptyMS I by A2;
then (K (/\) X) . i = {} by PBOOLE:5;
then Y9 /\ (X . i) = {} by A3, A8, PBOOLE:def 5;
hence Y9 misses X . i by XBOOLE_0:def 7; :: thesis: verum

end;

X . i c= (union (A (\/) B)) . i by A1, A3;
then X . i c= union ((A . i) \/ (B . i)) by A3, Lm6;
then X . i c= union (A . i) by A4, SETFAM_1:42;
hence X . i c= (union A) . i by A3, Def2; :: thesis: verum