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;
( dom xx = I & rng xx c= union (rng (bool M)) ) by A1, Th3, PARTFUN1:def 4;
hence x in Funcs I,(union (rng (bool M))) by 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 A4: I is empty ; :: thesis: ex b₁ being set st
for x being set holds
( x in b₁ iff x is ManySortedSubset of M )

take {([0] {} )} ; :: thesis: for x being set holds
( x in {([0] {} )} iff x is ManySortedSubset of M )
A5: 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 A4; :: thesis: verum

end;

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

reconsider M9 = M as ManySortedSet of {} by A4;
assume A6: x in {([0] {} )} ; :: thesis: x is ManySortedSubset of M
[0] {} c= M9

proof

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

end;

then reconsider y = [0] {} as ManySortedSubset of M9 by PBOOLE:def 23;
y is ManySortedSubset of M by A4;
hence x is ManySortedSubset of M by A6, 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
A7: y = x ;
y c= M by PBOOLE:def 23;
then y is empty-yielding by A5, PBOOLE:142;
then y = [0] {} by A4, PBOOLE:141;
hence x in {([0] {} )} by A7, TARSKI:def 1; :: thesis: verum

end;

end;

end;