let Y, X 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
A3: card Y <> card (Tarski-Class X) by A2;
A4: not Y, Tarski-Class X are_equipotent by A3, CARD_1:21;
thus Y in Tarski-Class X by A1, A4, Th8; :: thesis: verum