theorem :: CLASSES1:6

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