theorem :: ALTCAT_4:45

for C being category st ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds m is mono ) holds
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllMono C