:: deftheorem defines X+ FIELD_9:def 3 :
for R being Ring
for a being Element of R holds X+ a = rpoly (1,(- a));