theorem Th53: :: CLASSES2:53

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