let X, Y 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 Th24;
then card Y <> card (Tarski-Class X) ;
hence not Y, Tarski-Class X are_equipotent by CARD_1:5; :: thesis: verum