reconsider a = p as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
- a = - p by FIELD_8:1;
hence - (- p) = - (- a) by FIELD_8:1
.= p ;
:: thesis: verum