set q = npoly (F_Real,n);

now :: thesis: not npoly (F_Real,n) is with_roots

assume npoly (F_Real,n) is with_roots ; :: thesis: contradiction
then consider r being Element of F_Real such that
H: r is_a_root_of npoly (F_Real,n) by POLYNOM5:def 8;
eval ((npoly (F_Real,n)),r) = 0. F_Real by H, POLYNOM5:def 7;
hence contradiction by lem1; :: thesis: verum

end;

hence not npoly (F_Real,n) is with_roots ; :: thesis: verum