theorem Th12: :: POLYEQ_5:12

for z, a0, a1, a2 being Complex st a2 <> 0 holds
( ((a2 * (z |^ 2)) + (a1 * z)) + a0 = 0 iff ( z = (- (a1 / (2 * a2))) + ((2 -root (delta (a0,a1,a2))) / (2 * a2)) or z = (- (a1 / (2 * a2))) - ((2 -root (delta (a0,a1,a2))) / (2 * a2)) ) )