let N be set ; :: thesis:
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:
thus N in M by A1; :: thesis:
thus for X, Y being set st X in M & Y c= X holds
Y in M by A2; :: thesis:
thus for X being set st X in M holds
bool X in M :: thesis:

let X be set ; :: thesis:
assume X in M ; :: thesis:
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;

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

end;

end;

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