theorem :: POLYEQ_4:12

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