theorem :: ALTCAT_3:21

for C being category
for o1, o2 being Object of C
for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso