theorem :: POLYEQ_1:22

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