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