let C be category; :: thesis: for o1, o2 being object of (AllMono C)
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
m is mono
let o1, o2 be object of (AllMono C); :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
m is mono
let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies m is mono )
assume A1: <^o1,o2^> <> {} ; :: thesis: m is mono
reconsider p1 = o1, p2 = o2 as object of C by Def1;
reconsider p = m as Morphism of p1,p2 by A1, ALTCAT_2:34;
p in the Arrows of (AllMono C) . o1,o2 by A1;
then ( <^p1,p2^> <> {} & p is mono ) by Def1;
hence m is mono by A1, Th37; :: thesis: verum