theorem Th6: :: CAT_6:6

for C being CategoryStr holds
( C is with_left_identities iff C opp is with_right_identities )