theorem Th65: :: CLASSES1:65

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