let X be set ; :: thesis: the_universe_of {X} is Grothendieck of X
the_universe_of {X} = Tarski-Class (the_transitive-closure_of {X}) by YELLOW_6:def 1;
hence the_universe_of {X} is Grothendieck of X by Th8; :: thesis: verum