theorem Th2: :: POLYEQ_3:2

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 / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) holds
z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>)