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 A1: ( Y c= Tarski-Class X & card Y in card (Tarski-Class X) ) ; :: thesis: Y in Tarski-Class X
then card Y <> card (Tarski-Class X) ;
then not Y, Tarski-Class X are_equipotent by CARD_1:21;
hence Y in Tarski-Class X by A1, Th8; :: thesis: verum