theorem Th54: :: CLASSES2:54

for U1, U2 being Universe holds U1,U2 are_c=-comparable