theorem :: CLASSES4:79

for X being non empty set
for GX being Grothendieck of X
for G being Universe holds
( not X misses G or GX in G or G in GX ) by Th78, CLASSES2:52;