per cases ( not I is empty or I is empty ) ;

suppose A1: not I is empty ; :: thesis: ex b₁ being set st
for x being set holds
( x in b₁ iff x is ManySortedSubset of M )

consider X being set such that
A2: for e being set holds
( e in X iff ( e in Funcs I,(union (rng (bool M))) & S₁[e] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff x is ManySortedSubset of M )
thus for x being set holds
( x in X iff x is ManySortedSubset of M ) :: thesis: verum

proof

let x be set ; :: thesis: ( x in X iff x is ManySortedSubset of M )
thus ( x in X implies x is ManySortedSubset of M ) by A2; :: thesis: ( x is ManySortedSubset of M implies x in X )
assume A3: x is ManySortedSubset of M ; :: thesis: x in X

now

reconsider xx = x as ManySortedSubset of M by A3;
A4: dom xx = I by PARTFUN1:def 4;
rng xx c= union (rng (bool M)) by A1, Th3;
hence x in Funcs I,(union (rng (bool M))) by A4, FUNCT_2:def 2; :: thesis: S₁[x]
thus S₁[x] by A3; :: thesis: verum

end;

hence x in X by A2; :: thesis: verum

end;

end;

suppose A5: I is empty ; :: thesis: ex b₁ being set st
for x being set holds
( x in b₁ iff x is ManySortedSubset of M )

A6: M is empty-yielding

proof

let i be set ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or M . i is empty )
assume i in I ; :: thesis: M . i is empty
hence M . i is empty by A5; :: thesis: verum

end;

take {([0] {} )} ; :: thesis: for x being set holds
( x in {([0] {} )} iff x is ManySortedSubset of M )
thus for x being set holds
( x in {([0] {} )} iff x is ManySortedSubset of M ) :: thesis: verum

proof

let x be set ; :: thesis: ( x in {([0] {} )} iff x is ManySortedSubset of M )
thus ( x in {([0] {} )} implies x is ManySortedSubset of M ) :: thesis: ( x is ManySortedSubset of M implies x in {([0] {} )} )

proof

assume A7: x in {([0] {} )} ; :: thesis: x is ManySortedSubset of M
reconsider M' = M as ManySortedSet of by A5;
[0] {} is ManySortedSubset of M'

proof

thus [0] {} c= M' :: according to PBOOLE:def 23 :: thesis: verum

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in {} or ([0] {} ) . i c= M' . i )
assume i in {} ; :: thesis: ([0] {} ) . i c= M' . i
hence ([0] {} ) . i c= M' . i ; :: thesis: verum

end;

end;

then reconsider y = [0] {} as ManySortedSubset of M' ;
y is ManySortedSubset of M by A5;
hence x is ManySortedSubset of M by A7, TARSKI:def 1; :: thesis: verum

end;

assume x is ManySortedSubset of M ; :: thesis: x in {([0] {} )}
then consider y being ManySortedSubset of M such that
A8: y = x ;
y c= M by PBOOLE:def 23;
then y is empty-yielding by A6, PBOOLE:142;
then y = [0] {} by A5, PBOOLE:141;
hence x in {([0] {} )} by A8, TARSKI:def 1; :: thesis: verum

end;

end;

end;