let Y, X be set ; :: thesis: ( Y in Tarski-Class X implies not Y, Tarski-Class X are_equipotent )
assume Y in Tarski-Class X ; :: thesis: not Y, Tarski-Class X are_equipotent
then card Y in card (Tarski-Class X) by Th28;
then card Y <> card (Tarski-Class X) ;
hence not Y, Tarski-Class X are_equipotent by CARD_1:21; :: thesis: verum