theorem Th1: :: POLYEQ_3:1

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