let A, B be category; :: thesis: ( A,B are_anti-isomorphic implies A,B are_dual )
A1: B,B opp are_opposite by Def4;
assume A,B are_anti-isomorphic ; :: thesis: A,B are_dual
then A,B opp are_isomorphic by A1, Th17;
hence A,B opp are_equivalent by Th5; :: according to YELLOW18:def 6 :: thesis: verum