let A, B be category; :: thesis: ( A,B are_opposite implies A,B are_anti-isomorphic )
assume A,B are_opposite ; :: thesis: A,B are_anti-isomorphic
then dualizing-func A,B is bijective by Th16;
hence A,B are_anti-isomorphic by FUNCTOR0:def 41; :: thesis: verum