theorem Th62: :: CLASSES1:62

for X being set ex A being Ordinal st X c= Rank A