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 Th15;
hence A,B are_anti-isomorphic ; :: thesis: verum