:: deftheorem Def1 defines AllMono ALTCAT_4:def 1 :
for C being category
for b₂ being non empty transitive strict SubCatStr of C holds
( b₂ = AllMono C iff ( the carrier of b₂ = the carrier of C & the Arrows of b₂ cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b₂ . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) ) );