let C be category; ( ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds m is mono ) implies AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllMono C )
assume A1:
for o1, o2 being Object of C
for m being Morphism of o1,o2 holds m is mono
; AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllMono C
A2:
the carrier of (AllMono C) = the carrier of AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
by Def1;
A3:
the Arrows of (AllMono C) cc= the Arrows of C
by Def1;
hence
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllMono C
by A2, ALTCAT_2:25, PBOOLE:3; verum