let A, B, C be category; :: thesis: ( A,B are_dual & B,C are_dual implies A,C are_equivalent )
assume that
A1: A,B opp are_equivalent and
A2: B,C are_dual ; :: according to YELLOW18:def 6 :: thesis: A,C are_equivalent
C,B opp are_equivalent by A2, Def6;
hence A,C are_equivalent by A1, Th4; :: thesis: verum