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 )
A2: ( B,C are_dual iff B,C opp are_equivalent ) by Def6;
C,C opp are_opposite by Def4;
hence ( A,C are_equivalent iff B,C are_dual ) by A1, A2, Th26; :: thesis: verum