theorem Th37: :: ALTCAT_4:37

for C being non empty transitive AltCatStr
for D being non empty transitive SubCatStr of C
for o1, o2 being Object of C
for p1, p2 being Object of D
for m being Morphism of o1,o2
for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds
( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )