let X be set ; :: thesis: ( the_rank_of (Tarski-Class X) <> {} & the_rank_of (Tarski-Class X) is limit_ordinal )
A1: ( Tarski-Class X c= Rank (the_rank_of (Tarski-Class X)) & ( for A being Ordinal st Tarski-Class X c= Rank A holds
the_rank_of (Tarski-Class X) c= A ) ) by Def8;
thus the_rank_of (Tarski-Class X) <> {} :: thesis: the_rank_of (Tarski-Class X) is limit_ordinal

proof

assume the_rank_of (Tarski-Class X) = {} ; :: thesis: contradiction
then Tarski-Class X c= {} by Def8, Lm2;
hence contradiction ; :: thesis: verum

end;

assume not the_rank_of (Tarski-Class X) is limit_ordinal ; :: thesis: contradiction
then consider A being Ordinal such that
A2: the_rank_of (Tarski-Class X) = succ A by ORDINAL1:42;
consider Y being set such that
A3: ( Y in Tarski-Class X & the_rank_of Y = A ) by A2, Th80;
A4: ( bool Y in Tarski-Class X & the_rank_of (bool Y) = succ A ) by A3, Th7, Th71;
then bool Y c= Rank A by A1, A2, Th36;
then succ A c= A by A4, Def8;
then A in A by ORDINAL1:33;
hence contradiction ; :: thesis: verum