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 object holds
( x in b₁ iff x is ManySortedSubset of M )

consider X being set such that
A2: for e being object 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 object holds
( x in X iff x is ManySortedSubset of M )
let x be object ; :: 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 :: thesis: ( x in Funcs (I,(union (rng (bool M)))) & S₁[x] )

reconsider xx = x as ManySortedSubset of M by A3;
( dom xx = I & rng xx c= union (rng (bool M)) ) by A1, Th2, PARTFUN1:def 2;
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;

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

take {(EmptyMS {})} ; :: thesis: for x being object holds
( x in {(EmptyMS {})} iff x is ManySortedSubset of M )
let x be object ; :: thesis: ( x in {(EmptyMS {})} iff x is ManySortedSubset of M )
thus ( x in {(EmptyMS {})} implies x is ManySortedSubset of M ) :: thesis: ( x is ManySortedSubset of M implies x in {(EmptyMS {})} )

proof

reconsider M9 = M as ManySortedSet of {} by A4;
assume A5: x in {(EmptyMS {})} ; :: thesis: x is ManySortedSubset of M
reconsider y = EmptyMS {} as ManySortedSubset of M9 by PBOOLE:def 18;
y is ManySortedSubset of M by A4;
hence x is ManySortedSubset of M by A5, TARSKI:def 1; :: thesis: verum

end;

assume x is ManySortedSubset of M ; :: thesis: x in {(EmptyMS {})}
then consider y being ManySortedSubset of M such that
A6: y = x ;
y = EmptyMS {} by A4;
hence x in {(EmptyMS {})} by A6, TARSKI:def 1; :: thesis: verum

end;

end;