theorem :: CLASSES4:9

for X being set holds the_universe_of {X} is Grothendieck of X