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