theorem :: ALTCAT_3:24

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