let X, Y be set ; :: thesis: ( Y in Tarski-Class X implies card Y in card (Tarski-Class X) )
assume A1: Y in Tarski-Class X ; :: thesis: card Y in card (Tarski-Class X)
bool Y c= Tarski-Class X by A1, Th3;
then ( card Y in card (bool Y) & card (bool Y) c= card (Tarski-Class X) ) by CARD_1:11, CARD_1:14;
hence card Y in card (Tarski-Class X) ; :: thesis: verum