let A, B, C be category; :: thesis: ( A,B are_opposite implies ( A,C are_equivalent iff B,C are_dual ) )
assume A1: A,B are_opposite ; :: thesis: ( A,C are_equivalent iff B,C are_dual )
C,C opp are_opposite by Def4;
hence ( A,C are_equivalent iff B,C are_dual ) by A1, Th25; :: thesis: verum