theorem Th77: :: CLASSES4:77

( GrothendieckUniverse omega = GrothendieckUniverse FinSETS & GrothendieckUniverse FinSETS = SETS )