theorem Th4: :: CAT_6:4

for C being CategoryStr holds
( C is left_composable iff C opp is right_composable )