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 40; :: thesis: verum