theorem Th5: :: CAT_6:5

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