Tarski-Class A is_Tarski-Class_of A by Def4;
hence not Tarski-Class A is empty by Def3; :: thesis: verum