theorem :: CLASSES2:52

for U1, U2 being Universe holds
( U1 in U2 or U1 = U2 or U2 in U1 )