theorem :: CLASSES4:50

for G being non empty Grothendieck holds
( not G <> GrothendieckUniverse omega or GrothendieckUniverse omega in G or G in GrothendieckUniverse omega ) by CLASSES2:52;