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)) by Def8;
thus the_rank_of (Tarski-Class X) <> {} :: thesis: the_rank_of (Tarski-Class X) is limit_ordinal

proof

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

end;

assume A4: not the_rank_of (Tarski-Class X) is limit_ordinal ; :: thesis: contradiction
consider A being Ordinal such that
A5: the_rank_of (Tarski-Class X) = succ A by A4, ORDINAL1:42;
consider Y being set such that
A6: Y in Tarski-Class X and
A7: the_rank_of Y = A by A5, Th80;
A8: bool Y in Tarski-Class X by A6, Th7;
A9: the_rank_of (bool Y) = succ A by A7, Th71;
A10: bool Y c= Rank A by A1, A5, A8, Th36;
A11: succ A c= A by A9, A10, Def8;
A12: A in A by A11, ORDINAL1:33;
thus contradiction by A12; :: thesis: verum