let X be set ; :: thesis: Tarski-Class X is Tarski
Tarski-Class X is_Tarski-Class_of X by CLASSES1:def 4;
hence Tarski-Class X is Tarski by CLASSES1:def 3; :: thesis: verum