:: deftheorem Def4 defines " ALTCAT_3:def 4 :
for C being category
for o1, o2 being Object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
for b₅ being Morphism of o2,o1 holds
( b₅ = A " iff ( b₅ is_left_inverse_of A & b₅ is_right_inverse_of A ) );