theorem Th5: :: ALTCAT_3:5

for C being category
for o1, o2 being Object of C
for A being Morphism of o1,o2 st A is iso holds
( A is retraction & A is coretraction )