theorem :: POLYEQ_3:7

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