let X be set ; :: thesis: Tarski-Class (the_transitive-closure_of {X}) is Grothendieck of X
set R = the_transitive-closure_of {X};
set T = Tarski-Class (the_transitive-closure_of {X});
A1: union (Tarski-Class (the_transitive-closure_of {X})) c= Tarski-Class (the_transitive-closure_of {X}) by CLASSES1:48;
( X in {X} & {X} c= the_transitive-closure_of {X} ) by CLASSES1:52, TARSKI:def 1;
then ( X in the_transitive-closure_of {X} & the_transitive-closure_of {X} in Tarski-Class (the_transitive-closure_of {X}) ) by CLASSES1:2;
then X in union (Tarski-Class (the_transitive-closure_of {X})) by TARSKI:def 4;
hence Tarski-Class (the_transitive-closure_of {X}) is Grothendieck of X by A1, CLASSES3:def 4; :: thesis: verum