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