theorem Th21: :: CLASSES2:21

for W being set holds
( card (Tarski-Class W) <> 0 & card (Tarski-Class W) <> {} & card (Tarski-Class W) is limit_ordinal )