let A, B, C be category; :: thesis: ( 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 ; :: according to YELLOW18:def 6 :: thesis: 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; :: according to YELLOW18:def 6 :: thesis: verum