let C be category; :: thesis:
let D be non empty subcategory of C; :: thesis:
let o1, o2 be object of C; :: thesis:
let p1, p2 be object of D; :: thesis:
let m be Morphism of o1,o2; :: thesis:
let n be Morphism of p1,p2; :: thesis:
assume A1: ( p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} ) ; :: thesis:
thus A2: ( n is retraction implies m is retraction ) :: thesis:

proof

assume n is retraction ; :: thesis:
then consider B being Morphism of p2,p1 such that
A3: B is_right_inverse_of n by ALTCAT_3:def 2;
reconsider B1 = B as Morphism of o2,o1 by A1, ALTCAT_2:34;
take B1 ; :: according to ALTCAT_3:def 2 :: thesis:
thus m is_left_inverse_of B1 by A1, A3, Th38; :: thesis:

end;

thus A4: ( n is coretraction implies m is coretraction ) :: thesis:

proof

assume n is coretraction ; :: thesis:
then consider B being Morphism of p2,p1 such that
A5: B is_left_inverse_of n by ALTCAT_3:def 3;
reconsider B1 = B as Morphism of o2,o1 by A1, ALTCAT_2:34;
take B1 ; :: according to ALTCAT_3:def 3 :: thesis:
thus B1 is_left_inverse_of m by A1, A5, Th38; :: thesis:

end;

assume A6: n is iso ; :: thesis:
( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A1, ALTCAT_2:32, XBOOLE_1:3;
hence m is iso by A2, A4, A6, ALTCAT_3:5, ALTCAT_3:6; :: thesis: