theorem Th12: :: CAT_6:12

for C being CategoryStr holds
( C is left_composable iff CategoryStr(# the carrier of C, the composition of C #) is left_composable )