theorem Th50: :: ALTCAT_4:50
for C being category
for o1, o2 being Object of (AllMono C)
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
m is mono