let X, Y be set ; :: thesis: ( Y in Tarski-Class X implies bool Y in Tarski-Class X )
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is Tarski ;
hence ( Y in Tarski-Class X implies bool Y in Tarski-Class X ) ; :: thesis: verum