theorem Th66: :: CLASSES1:66

for X being set
for A being Ordinal holds
( X in Rank A iff the_rank_of X in A )