for C being category
for D being non empty subcategory 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^> <> {} & <^p2,p1^> <> {} holds
( ( n is retraction implies m is retraction ) & ( n is coretraction implies m is coretraction ) & ( n is iso implies m is iso ) )