per cases ( not I is empty or I is empty ) ;
suppose A1: not I is empty ; :: thesis: ex b1 being set st
for x being object holds
( x in b1 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)))) & S1[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)))) & S1[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: S1[x]
thus S1[x] by A3; :: thesis: verum
end;
hence x in X by A2; :: thesis: verum
end;
suppose A4: I is empty ; :: thesis: ex b1 being set st
for x being object holds
( x in b1 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;