let W be set ; :: thesis: ( W is Tarski implies Rank (card W) c= W )
assume A1: W is Tarski ; :: thesis: Rank (card W) c= W
then A2: W is subset-closed ;

now

assume A3: W <> {} ; :: thesis: Rank (card W) c= W
thus Rank (card W) c= W :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Rank (card W) or x in W )
assume A4: x in Rank (card W) ; :: thesis: x in W
( card W <> {} & card W is limit_ordinal ) by A1, A3, Th21;
then consider A being Ordinal such that
A5: ( A in card W & x in Rank A ) by A4, CLASSES1:35;
A in On W by A1, A5, Th10;
then ( Rank A in W & Rank A is epsilon-transitive ) by A1, Th26;
then Rank A c= W by A2, Th8;
hence x in W by A5; :: thesis: verum

end;

end;

hence Rank (card W) c= W by CLASSES1:33; :: thesis: verum