theorem :: QUIN_1:22
for x, a, b, c being Real st a > 0 & delta (a,b,c) = 0 holds
( ((a * (x ^2)) + (b * x)) + c > 0 iff x <> - (b / (2 * a)) )