theorem Th20: :: ALTCAT_4:20

for A, B being category
for F being covariant Functor of A,B
for o1, o2 being Object of A
for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds
F . a is iso