let A, B, C be category; :: thesis: ( A,B are_opposite implies ( A,C are_isomorphic iff B,C are_anti-isomorphic ) )
assume A,B are_opposite ; :: thesis: ( A,C are_isomorphic iff B,C are_anti-isomorphic )
then A1: dualizing-func A,B is bijective by Th16;

hereby :: thesis: ( B,C are_anti-isomorphic implies A,C are_isomorphic )

assume A,C are_isomorphic ; :: thesis: B,C are_anti-isomorphic
then consider F being Functor of C,A such that
A2: ( F is bijective & F is covariant ) by FUNCTOR0:def 40;
reconsider F = F as covariant Functor of C,A by A2;
( (dualizing-func A,B) * F is bijective & (dualizing-func A,B) * F is contravariant ) by A1, A2, FUNCTOR1:13;
hence B,C are_anti-isomorphic by FUNCTOR0:def 41; :: thesis: verum

end;

assume B,C are_anti-isomorphic ; :: thesis: A,C are_isomorphic
then consider F being Functor of B,C such that
A3: ( F is bijective & F is contravariant ) by FUNCTOR0:def 41;
reconsider F = F as contravariant Functor of B,C by A3;
( F * (dualizing-func A,B) is bijective & F * (dualizing-func A,B) is covariant ) by A1, A3, FUNCTOR1:13;
hence A,C are_isomorphic by FUNCTOR0:def 40; :: thesis: verum