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