set GU0 = GrothendieckUniverse {};
set GUomega = GrothendieckUniverse omega;
( the empty Grothendieck c= omega & omega c= GrothendieckUniverse {} & GrothendieckUniverse {} c= GrothendieckUniverse omega ) by Th16, CLASSES3:21;
hence ( the empty Grothendieck c< omega & omega c< GrothendieckUniverse {} & GrothendieckUniverse {} c< GrothendieckUniverse omega ) by Th46, Th43, Th19, Th20, CLASSES3:def 4; :: thesis: verum