theorem :: CLASSES2:26

for A being Ordinal
for W being set st A in On (Tarski-Class W) holds
( card (Rank A) in card (Tarski-Class W) & Rank A in Tarski-Class W ) by Th25;