set p = 1_. R;
assume 1_. R is with_roots ; :: thesis: contradiction
then consider x being Element of R such that
A: x is_a_root_of 1_. R by POLYNOM5:def 8;
0. R = eval ((1_. R),x) by A, POLYNOM5:def 7
.= 1. R by POLYNOM4:18 ;
hence contradiction ; :: thesis: verum