theorem Th3: :: ALTCAT_4:3

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