theorem :: CLASSES1:39

for A being Ordinal
for X being set st X in Rank A holds
( not X, Rank A are_equipotent & card X in card (Rank A) )