theorem :: QUIN_1:27

for x, a, b, c being Real st a > 0 & delta (a,b,c) > 0 holds
( ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) iff ((a * (x ^2)) + (b * x)) + c > 0 )