theorem :: CLASSES4:51

Tarski-Class omega = GrothendieckUniverse omega by CLASSES3:22;