theorem :: CLASSES4:49

( the empty Grothendieck c< omega & omega c< GrothendieckUniverse {} & GrothendieckUniverse {} c< GrothendieckUniverse omega )