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

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