let X be set ; :: thesis: X in Tarski-Class X
A1: Tarski-Class X is_Tarski-Class_of X by Def4;
thus X in Tarski-Class X by A1, Def3; :: thesis: verum