let a, b, c be Real; ( ( 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
; 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, Th6;
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; verum