GrothendieckUniverse omega = GrothendieckUniverse FinSETS

proof

GrothendieckUniverse omega = SETS by CLASSES3:22, Th75;
hence GrothendieckUniverse omega = GrothendieckUniverse FinSETS by CLASSES3:22; :: thesis: verum

end;

hence ( GrothendieckUniverse omega = GrothendieckUniverse FinSETS & GrothendieckUniverse FinSETS = SETS ) by CLASSES3:22; :: thesis: verum