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