theorem Th24: :: CLASSES1:24

for X, Y being set st Y in Tarski-Class X holds
card Y in card (Tarski-Class X)