let A, B be category; :: thesis: ( A,B opp are_equivalent implies B,A opp are_equivalent )
A1: A,A opp are_opposite by Def4;
B,B opp are_opposite by Def4;
hence ( A,B opp are_equivalent implies B,A opp are_equivalent ) by A1, Th25; :: thesis: verum