theorem :: ALTCAT_4:6

for C being category st ( for o1, o2 being Object of C
for f being Morphism of o1,o2 holds f is coretraction ) holds
for a, b being Object of C
for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
g is iso