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

now :: thesis: ( W <> {} implies Rank (card W) c= W )

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

proof

A3: card W is limit_ordinal by A1, Th19;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Rank (card W) or x in W )
assume x in Rank (card W) ; :: thesis: x in W
then consider A being Ordinal such that
A4: A in card W and
A5: x in Rank A by A2, A3, CLASSES1:31;
A in On W by A1, A4, Th9;
then Rank A c= W by A1, Th7, Th25;
hence x in W by A5; :: thesis: verum

end;

end;

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