let X be set ; :: thesis: X in Tarski-Class X
Tarski-Class X is_Tarski-Class_of X by Def4;
hence X in Tarski-Class X ; :: thesis: verum