theorem Th25: :: CLASSES2:25

for A being Ordinal
for W being set st W is Tarski & A in On W holds
( card (Rank A) in card W & Rank A in W )