let W, X be set ; :: thesis: ( W is Tarski & X in W implies Tarski-Class X c= W )
assume A1: ( W is Tarski & X in W ) ; :: thesis: Tarski-Class X c= W
then reconsider D = W as non empty set ;
D is_Tarski-Class_of X by A1, CLASSES1:def 3;
hence Tarski-Class X c= W by CLASSES1:def 4; :: thesis: verum