let a, b, c be Real; :: thesis: ( delta (a,b,c) < 0 implies for x being Real holds not Polynom (a,b,c,x) = 0 )

set e = a * c;

assume delta (a,b,c) < 0 ; :: thesis: for x being Real holds not Polynom (a,b,c,x) = 0

then (b ^2) - ((4 * a) * c) < 0 by QUIN_1:def 1;

then A1: ((b ^2) - (4 * (a * c))) * (4 ") < 0 by XREAL_1:132;

given y being Real such that A2: Polynom (a,b,c,y) = 0 ; :: thesis: contradiction

set t = ((a ^2) * (y ^2)) + ((a * b) * y);

a * (((a * (y ^2)) + (b * y)) + c) = a * 0 by A2;

then ((((a ^2) * (y ^2)) + ((a * b) * y)) + ((b ^2) / 4)) - (((b ^2) * (4 ")) - ((4 * (a * c)) * (4 "))) = 0 ;

then A3: ((a * y) + (b / 2)) ^2 = ((b ^2) - (4 * (a * c))) * (4 ") ;

then (a * y) + (b / 2) > 0 by A1, XREAL_1:133;

hence contradiction by A3, A1, XREAL_1:133; :: thesis: verum

set e = a * c;

assume delta (a,b,c) < 0 ; :: thesis: for x being Real holds not Polynom (a,b,c,x) = 0

then (b ^2) - ((4 * a) * c) < 0 by QUIN_1:def 1;

then A1: ((b ^2) - (4 * (a * c))) * (4 ") < 0 by XREAL_1:132;

given y being Real such that A2: Polynom (a,b,c,y) = 0 ; :: thesis: contradiction

set t = ((a ^2) * (y ^2)) + ((a * b) * y);

a * (((a * (y ^2)) + (b * y)) + c) = a * 0 by A2;

then ((((a ^2) * (y ^2)) + ((a * b) * y)) + ((b ^2) / 4)) - (((b ^2) * (4 ")) - ((4 * (a * c)) * (4 "))) = 0 ;

then A3: ((a * y) + (b / 2)) ^2 = ((b ^2) - (4 * (a * c))) * (4 ") ;

then (a * y) + (b / 2) > 0 by A1, XREAL_1:133;

hence contradiction by A3, A1, XREAL_1:133; :: thesis: verum