let a, b, c be Real; :: thesis: ( ( for x being Real holds ((a * (x ^2)) + (b * x)) + c <= 0 ) & a < 0 implies delta (a,b,c) <= 0 )

assume that

A1: for x being Real holds ((a * (x ^2)) + (b * x)) + c <= 0 and

A2: a < 0 ; :: thesis: delta (a,b,c) <= 0

((a * ((- (b / (2 * a))) ^2)) + (b * (- (b / (2 * a))))) + c <= 0 by A1;

then ((((2 * a) * (- (b / (2 * a)))) + b) ^2) - (delta (a,b,c)) >= 0 by A2, Th8;

then A3: (((- ((2 * a) * (b / (2 * a)))) + b) ^2) - (delta (a,b,c)) >= 0 ;

2 * a <> 0 by A2;

then (((- b) + b) ^2) - (delta (a,b,c)) >= 0 by A3, XCMPLX_1:87;

then - (delta (a,b,c)) >= - 0 ;

hence delta (a,b,c) <= 0 by XREAL_1:24; :: thesis: verum

assume that

A1: for x being Real holds ((a * (x ^2)) + (b * x)) + c <= 0 and

A2: a < 0 ; :: thesis: delta (a,b,c) <= 0

((a * ((- (b / (2 * a))) ^2)) + (b * (- (b / (2 * a))))) + c <= 0 by A1;

then ((((2 * a) * (- (b / (2 * a)))) + b) ^2) - (delta (a,b,c)) >= 0 by A2, Th8;

then A3: (((- ((2 * a) * (b / (2 * a)))) + b) ^2) - (delta (a,b,c)) >= 0 ;

2 * a <> 0 by A2;

then (((- b) + b) ^2) - (delta (a,b,c)) >= 0 by A3, XCMPLX_1:87;

then - (delta (a,b,c)) >= - 0 ;

hence delta (a,b,c) <= 0 by XREAL_1:24; :: thesis: verum