theorem :: CLASSES2:33
for A being Ordinal
for W being set st A in On (Tarski-Class W) holds
card (Rank A) c= card (Tarski-Class W)