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 ; :: thesis: verum