theorem Th35: :: CAT_7:35

for C1, C2 being composable with_identities CategoryStr st C1 ~= C2 holds
RelOb C1, RelOb C2 are_isomorphic