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

hence
Roots p is empty
; :: thesis: verumassume 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;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