theorem :: CLASSES2:55

for U1, U2 being Universe holds
( U1 \/ U2 is Universe & U1 /\ U2 is Universe )