let x, a, b, c be Real; :: thesis: ( 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 ; :: thesis: ((((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:128;
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; :: thesis: verum