theorem :: CLASSES4:76

GrothendieckUniverse omega = SETS by CLASSES3:22, Th75;