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