theorem :: ALTCAT_3:11

for C being non empty transitive associative AltCatStr
for o1, o2, o3 being Object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is mono holds
A is mono