theorem :: POLYEQ_4:13

for x, a, b, c being Real st a <> 0 & (((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c) > 0 & Polynom (a,b,c,c,b,a,x) = 0 holds
for y1, y2 being Real st y1 = ((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & y2 = ((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & not x = - 1 & not x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 & not x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 & not x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 holds
x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2