A,A opp are_opposite by Def4;
hence dualizing-func ((A opp),A) is bijective by Th15; :: thesis: verum