ex x being Element of R st x is_a_root_of p by POLYNOM5:def 8;
hence not Roots p is empty by POLYNOM5:def 10; :: thesis: verum