theorem Th46: :: CLASSES4:46
( GrothendieckUniverse {} = FinSETS & GrothendieckUniverse {} = UNIVERSE {} ) by Th45, CLASSES2:65, CLASSES2:56, CLASSES3:21;