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 ) )
thus ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) ) by A1, 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
A4: card X <> card W by A3;
A5: not X,W are_equipotent by A4, CARD_1:21;
thus X in W by A1, A2, A5, Def2; :: thesis: verum

end;

A6: now

assume A7: 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 A8: X c= W ; :: thesis: ( X,W are_equipotent or X in W )
A9: ( ( card X c= card W & not card X in card W ) or X in W ) by A7, A8, CARD_1:27;
A10: ( card X = card W or X in W ) by A9, CARD_1:13;
thus ( X,W are_equipotent or X in W ) by A10, CARD_1:21; :: thesis: verum

end;

thus ( 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 A6, Def2; :: thesis: verum