let X, Y be set ; :: thesis: ( Y c= Tarski-Class X & card Y in card (Tarski-Class X) implies Y in Tarski-Class X )
assume that
A1: Y c= Tarski-Class X and
A2: card Y in card (Tarski-Class X) ; :: thesis: Y in Tarski-Class X
card Y <> card (Tarski-Class X) by A2;
hence Y in Tarski-Class X by A1, Th5, CARD_1:5; :: thesis: verum