theorem :: POLYEQ_1:20

for b, c, d, x being Real st b <> 0 & delta (b,c,d) > 0 & Polynom (0,b,c,d,x) = 0 & not x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) holds
x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b)