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)
A2: 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 A3: x in bool Y ; :: thesis: x in Tarski-Class X
thus x in Tarski-Class X by A1, A3, Th6; :: thesis: verum

end;

A4: ( card Y in card (bool Y) & card (bool Y) c= card (Tarski-Class X) ) by A2, CARD_1:27, CARD_1:30;
thus card Y in card (Tarski-Class X) by A4; :: thesis: verum