theorem :: CLASSES2:65

UNIVERSE {} = FinSETS by Lm6;