let W be set ; :: thesis: ( W is Tarski iff ( 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 ) ) )

hereby :: thesis: ( 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 )

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

end;

now

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

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 ) by Def2; :: thesis: verum