theorem :: CLASSES4:10

for X being set holds Universe_closure {X} = GrothendieckUniverse X