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