theorem :: CLASSES2:10

for W being set holds On (Tarski-Class W) = card (Tarski-Class W) by Th9;