theorem Th30: :: ALTCAT_4:30

for A, B being non empty transitive with_units AltCatStr
for F being contravariant Functor of A,B
for o1, o2 being Object of A
for a being Morphism of o1,o2 st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is retraction holds
a is coretraction