theorem Th8: :: CLASSES4:8

for X being set holds Tarski-Class (the_transitive-closure_of {X}) is Grothendieck of X