theorem Th3: :: CAT_8:3

for C being composable CategoryStr
for f, f1, f2 being morphism of C st f1 |> f2 holds
( ( f1 (*) f2 |> f implies f2 |> f ) & ( f2 |> f implies f1 (*) f2 |> f ) & ( f |> f1 (*) f2 implies f |> f1 ) & ( f |> f1 implies f |> f1 (*) f2 ) )