let W be set ; :: thesis: ( W is Tarski implies Rank (card W) is Tarski )
assume A1: W is Tarski ; :: thesis: Rank (card W) is Tarski
set B = Rank (card W);
thus for X, Y being set st X in Rank (card W) & Y c= X holds
Y in Rank (card W) by CLASSES1:41; :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis: ( ( for b₁ being set holds
( not b₁ in Rank (card W) or bool b₁ in Rank (card W) ) ) & ( for b₁ being set holds
( not b₁ c= Rank (card W) or b₁, Rank (card W) are_equipotent or b₁ in Rank (card W) ) ) )

now :: thesis: ( W <> {} implies for X being set st X in Rank (card W) holds
bool X in Rank (card W) )

A2: card W is limit_ordinal by A1, Th19;
assume A3: W <> {} ; :: thesis: for X being set st X in Rank (card W) holds
bool X in Rank (card W)
thus for X being set st X in Rank (card W) holds
bool X in Rank (card W) :: thesis: verum

proof

let X be set ; :: thesis: ( X in Rank (card W) implies bool X in Rank (card W) )
assume X in Rank (card W) ; :: thesis: bool X in Rank (card W)
then consider A being Ordinal such that
A4: A in card W and
A5: X in Rank A by A3, A2, CLASSES1:31;
A6: bool X in Rank (succ A) by A5, CLASSES1:42;
succ A in card W by A2, A4, ORDINAL1:28;
hence bool X in Rank (card W) by A2, A6, CLASSES1:31; :: thesis: verum

end;

end;

hence ( ( for b₁ being set holds
( not b₁ in Rank (card W) or bool b₁ in Rank (card W) ) ) & ( for b₁ being set holds
( not b₁ c= Rank (card W) or b₁, Rank (card W) are_equipotent or b₁ in Rank (card W) ) ) ) by A1, Th36, CLASSES1:29; :: thesis: verum