now :: thesis: ( Roots p <> {} implies for u being Element of Roots p holds contradiction )

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

end;

hence Roots p is empty ; :: thesis: verum