let a, b, c be real number ; :: thesis: ( a <> 0 & delta a,b,c < 0 implies for x being real number holds not Polynom a,b,c,x = 0 )
assume A1: ( a <> 0 & delta a,b,c < 0 ) ; :: thesis: for x being real number holds not Polynom a,b,c,x = 0
given y being real number such that A2: Polynom a,b,c,y = 0 ; :: thesis: contradiction
A3: a * (((a * (y ^2 )) + (b * y)) + c) = a * 0 by A2;
set t = ((a ^2 ) * (y ^2 )) + ((a * b) * y);
set e = a * c;
((((a ^2 ) * (y ^2 )) + ((a * b) * y)) + ((b ^2 ) / 4)) - (((b ^2 ) * (4 " )) - ((4 * (a * c)) * (4 " ))) = 0 by A3;
then A4: ((a * y) + (b / 2)) ^2 = ((b ^2 ) - (4 * (a * c))) * (4 " ) ;
(b ^2 ) - ((4 * a) * c) < 0 by A1, QUIN_1:def 1;
then ((b ^2 ) - (4 * (a * c))) * (4 " ) < 0 by XREAL_1:134;
then ( (a * y) + (b / 2) > 0 & (a * y) + (b / 2) < 0 ) by A4, XREAL_1:135;
hence contradiction ; :: thesis: verum