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