theorem Th7: :: CAT_6:7

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