let Y, X, Z be set ; :: thesis: ( Y in Tarski-Class X & Z c= Y implies Z in Tarski-Class X )
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is Tarski by Def3;
then Tarski-Class X is subset-closed by Def2;
hence ( Y in Tarski-Class X & Z c= Y implies Z in Tarski-Class X ) by Def1; :: thesis: verum