theorem :: QUIN_1:19

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 )