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 Th15;

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 39;
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:12;
hence B,C are_anti-isomorphic by FUNCTOR0:def 40; :: 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 ) ;
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:12;
hence A,C are_isomorphic ; :: thesis: verum