let x, a, b, c be Real; ( a < 0 & ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 implies ((a * (x ^2)) + (b * x)) + c < 0 )
assume that
A1:
a < 0
and
A2:
((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0
; ((a * (x ^2)) + (b * x)) + c < 0
4 * a <> 0
by A1;
then A3:
((((2 * a) * x) + b) ^2) - ((4 * a) * ((delta (a,b,c)) / (4 * a))) > 0
by A2, XCMPLX_1:87;
2 * a <> 0
by A1;
then
((((2 * a) * x) + ((2 * a) * (b / (2 * a)))) ^2) - ((4 * a) * ((delta (a,b,c)) / (4 * a))) > 0
by A3, XCMPLX_1:87;
then A4:
(4 * a) * ((a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a))) > 0
;
4 * a < 0
by A1, XREAL_1:132;
then
(a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a)) < 0 / (4 * a)
by A4, XREAL_1:84;
hence
((a * (x ^2)) + (b * x)) + c < 0
by A1, Th1; verum