theorem :: CLASSES4:47

for X being set
for G being Grothendieck of X holds
( GrothendieckUniverse {} c= GrothendieckUniverse X & GrothendieckUniverse X c= G ) by CLASSES2:56, CLASSES3:21, CLASSES3:def 5;