let W be set ; :: thesis:

hereby :: thesis:

assume A1: W is Tarski ; :: thesis:
hence ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) ) ; :: thesis:
let X be set ; :: thesis:
assume that
A2: X c= W and
A3: card X in card W ; :: thesis:
card X <> card W by A3;
then not X,W are_equipotent by CARD_1:5;
hence X in W by A1, A2; :: thesis:

end;

now :: thesis:

assume A4: for X being set st X c= W & card X in card W holds
X in W ; :: thesis:
let X be set ; :: thesis:
assume X c= W ; :: thesis:
then ( ( card X c= card W & not card X in card W ) or X in W ) by A4, CARD_1:11;
hence ( X,W are_equipotent or X in W ) by CARD_1:3, CARD_1:5; :: thesis:

end;

hence ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) & ( for X being set st X c= W & card X in card W holds
X in W ) implies W is Tarski ) ; :: thesis: