theorem Th11: :: POLYEQ_5:11

for z, a0, a1, s1, s2 being Complex st a1 = - (s1 + s2) & a0 = s1 * s2 holds
( ((z |^ 2) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 ) )