theorem :: POLYEQ_2:3

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