let N be set ; :: thesis: ex M being set st
( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
consider M being set such that
A1: N in M and
A2: for X, Y being set st X in M & Y c= X holds
Y in M and
A3: for X being set st X in M holds
ex Z being set st
( Z in M & ( for Y being set st Y c= X holds
Y in Z ) ) and
A4: for X being set holds
( not X c= M or X,M are_equipotent or X in M ) by TARSKI_A:1;
take M ; :: thesis: ( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
thus N in M by A1; :: thesis: ( ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
thus for X, Y being set st X in M & Y c= X holds
Y in M by A2; :: thesis: ( ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )
thus for X being set st X in M holds
bool X in M :: thesis: for X being set holds
( not X c= M or X,M are_equipotent or X in M )

proof

let X be set ; :: thesis: ( X in M implies bool X in M )
assume X in M ; :: thesis: bool X in M
then consider Z being set such that
A5: Z in M and
A6: for Y being set st Y c= X holds
Y in Z by A3;

now :: thesis: for Y being object st Y in bool X holds
Y in Z

let Y be object ; :: thesis: ( Y in bool X implies Y in Z )
reconsider YY = Y as set by TARSKI:1;
assume Y in bool X ; :: thesis: Y in Z
then YY c= X by Def1;
hence Y in Z by A6; :: thesis: verum

end;

hence bool X in M by A2, A5, TARSKI:def 3; :: thesis: verum

end;

thus for X being set holds
( not X c= M or X,M are_equipotent or X in M ) by A4; :: thesis: verum