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
( B,B opp are_opposite & C,C opp are_opposite ) by Def4;
then B opp ,C opp are_equivalent by A2, Th26;
hence A,C opp are_equivalent by A1, Th4; :: according to YELLOW18:def 6 :: thesis: verum