:: deftheorem defines mono ALTCAT_3:def 7 :
for C being non empty AltCatStr
for o1, o2 being Object of C
for A being Morphism of o1,o2 holds
( A is mono iff for o being Object of C st <^o,o1^> <> {} holds
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C );