theorem Th2: :: POLYEQ_2:2

for a, b, c, x, y being Real st a <> 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 holds
( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 )