let Y, X be set ; :: thesis: ( Y in Tarski-Class X implies bool Y in Tarski-Class X )
A1: Tarski-Class X is_Tarski-Class_of X by Def4;
A2: Tarski-Class X is Tarski by A1, Def3;
thus ( Y in Tarski-Class X implies bool Y in Tarski-Class X ) by A2, Def2; :: thesis: verum