let Y, X 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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool Y or x in Tarski-Class X )
assume x in bool Y ; :: thesis: x in Tarski-Class X
hence x in Tarski-Class X by A1, Th6; :: thesis: verum

end;

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