theorem :: CLASSES1:74

for X being set holds
( the_rank_of (Tarski-Class X) <> {} & the_rank_of (Tarski-Class X) is limit_ordinal )