set e = a * c;
let y be Real; :: thesis: ( not Polynom (a,b,c,y) = 0 or y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) )
set t = ((a ^2) * (y ^2)) + ((a * b) * y);
assume Polynom (a,b,c,y) = 0 ; :: thesis: ( y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) )
then a * (((a * (y ^2)) + (b * y)) + c) = a * 0 ;
then ((a * (a * (y ^2))) + (a * (b * y))) + (a * c) = 0 ;
then A3: ((((a ^2) * (y ^2)) + ((a * b) * y)) + ((b ^2) / 4)) - ((b ^2) * (4 ")) = - ((4 * (a * c)) * (4 ")) ;
A4: delta (a,b,c) = (b ^2) - ((4 * a) * c) by QUIN_1:def 1;
((b ^2) - (4 * (a * c))) / 4 >= 0 / 4 by A2, A4, XREAL_1:72;
then ((a * y) + (b / 2)) ^2 = (sqrt (((b ^2) - (4 * (a * c))) / 4)) ^2 by A3, SQUARE_1:def 2;
then (((a * y) + (b / 2)) - (sqrt (((b ^2) - (4 * (a * c))) / 4))) * (((a * y) + (b / 2)) + (sqrt (((b ^2) - (4 * (a * c))) / 4))) = 0 ;
hence ( y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) by A5, A6, XCMPLX_1:6; :: thesis: verum