let A, B, C be category; ( A,B are_dual & B,C are_equivalent implies A,C are_dual )
assume that
A1:
A,B opp are_equivalent
and
A2:
B,C are_equivalent
; YELLOW18:def 6 A,C are_dual
A3:
B,B opp are_opposite
by Def4;
C,C opp are_opposite
by Def4;
then
B opp ,C opp are_equivalent
by A2, A3, Th25;
hence
A,C opp are_equivalent
by A1, Th4; YELLOW18:def 6 verum