let a, b, c be real number ; :: thesis: ( ( for x being real number holds ((a * (x ^2 )) + (b * x)) + c < 0 ) & a < 0 implies delta a,b,c < 0 )
assume that
A1: for x being real number holds ((a * (x ^2 )) + (b * x)) + c < 0 and
A2: a < 0 ; :: thesis: delta a,b,c < 0
A3: 2 * a <> 0 by A2;

now

((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, Th9;
then (((- ((2 * a) * (b / (2 * a)))) + b) ^2 ) - (delta a,b,c) > 0 ;
then (((- b) + b) ^2 ) - (delta a,b,c) > 0 by A3, XCMPLX_1:88;
then - (delta a,b,c) > - 0 ;
hence delta a,b,c < 0 by XREAL_1:26; :: thesis: verum

end;

hence delta a,b,c < 0 ; :: thesis: verum