theorem Th34: :: CAT_7:34

for C being composable with_identities CategoryStr holds
( dom (RelOb C) = Ob C & rng (RelOb C) = Ob C )