let Y, X be set ; :: thesis: ( not Y c= Tarski-Class X or Y, Tarski-Class X are_equipotent or Y in Tarski-Class X )
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is Tarski by Def3;
hence ( not Y c= Tarski-Class X or Y, Tarski-Class X are_equipotent or Y in Tarski-Class X ) by Def2; :: thesis: verum