theorem Th69: :: CLASSES1:69

for X being set
for A being Ordinal holds
( the_rank_of X c= A iff for Y being set st Y in X holds
the_rank_of Y in A )