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