theorem :: ALTCAT_4:29

for A, B being category
for F being covariant Functor of A,B
for o1, o2 being Object of A st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o1,F . o2 are_iso holds
o1,o2 are_iso