theorem :: CLASSES2:67

UNIVERSE 1 = SETS by Lm6, Lm7;