assume A: Roots p <> {} ; :: thesis: for u being Element of Roots p holds contradiction
let u be Element of Roots p; :: thesis: contradiction
u in Roots p by A;
then reconsider x = u as Element of R ;
x is_a_root_of p by A, POLYNOM5:def 10;
hence contradiction by POLYNOM5:def 8; :: thesis: verum