let o1, o2 be Object of C; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso implies ( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso ) )
assume that
A3: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) and
A4: ex A being Morphism of o1,o2 st A is iso ; :: thesis: ( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso )
thus ( <^o2,o1^> <> {} & <^o1,o2^> <> {} ) by A3; :: thesis: ex A being Morphism of o2,o1 st A is iso
consider A being Morphism of o1,o2 such that
A5: A is iso by A4;
take A1 = A " ; :: thesis: A1 is iso
A6: ( A is retraction & A is coretraction ) by A5, Th5;
then A7: (A1 ") * A1 = A * (A ") by A3, Th3
.= idm o2 by A3, A6, Th2 ;
A1 * (A1 ") = (A ") * A by A3, A6, Th3
.= idm o1 by A3, A6, Th2 ;
hence A1 is iso by A7; :: thesis: verum