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 or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) ) )
assume that
A1: a <> 0 and
A2: delta a,b,c >= 0 ; :: thesis: for x being real number holds
( not Polynom a,b,c,x = 0 or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) )

now

set e = a * c;
let y be real number ; :: 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;

A5: now

assume ((a * y) + (b / 2)) - (sqrt (((b ^2 ) - (4 * (a * c))) / 4)) = 0 ; :: thesis: y = ((- b) + (sqrt (delta a,b,c))) / (2 * a)
then (a * y) + (b / 2) = (sqrt ((b ^2 ) - (4 * (a * c)))) / 2 by A2, A4, SQUARE_1:85, SQUARE_1:99;
then a * y = - ((b * (2 " )) - ((sqrt ((b ^2 ) - (4 * (a * c)))) * (2 " )))
.= ((- b) * (2 " )) + ((sqrt (delta a,b,c)) * (2 " )) by A4 ;
then y = (((- b) * (2 " )) + ((sqrt (delta a,b,c)) * (2 " ))) / a by A1, XCMPLX_1:90
.= (((- b) * (2 " )) + ((sqrt (delta a,b,c)) * (2 " ))) * (a " ) by XCMPLX_0:def 9
.= ((- b) + (sqrt (delta a,b,c))) * ((2 " ) * (a " ))
.= ((- b) + (sqrt (delta a,b,c))) * ((2 * a) " ) by XCMPLX_1:205 ;
hence y = ((- b) + (sqrt (delta a,b,c))) / (2 * a) by XCMPLX_0:def 9; :: thesis: verum

end;

A6: now

assume ((a * y) + (b / 2)) + (sqrt (((b ^2 ) - (4 * (a * c))) / 4)) = 0 ; :: thesis: y = ((- b) - (sqrt (delta a,b,c))) / (2 * a)
then (a * y) + (b / 2) = - (sqrt (((b ^2 ) - (4 * (a * c))) / 4)) ;
then (a * y) + (b / 2) = - ((sqrt ((b ^2 ) - (4 * (a * c)))) / 2) by A2, A4, SQUARE_1:85, SQUARE_1:99;
then a * y = - ((b * (2 " )) + ((sqrt ((b ^2 ) - (4 * (a * c)))) * (2 " )))
.= ((- b) * (2 " )) - ((sqrt (delta a,b,c)) * (2 " )) by A4 ;
then y = (((- b) * (2 " )) - ((sqrt (delta a,b,c)) * (2 " ))) / a by A1, XCMPLX_1:90
.= (((- b) * (2 " )) - ((sqrt (delta a,b,c)) * (2 " ))) * (a " ) by XCMPLX_0:def 9
.= ((- b) - (sqrt (delta a,b,c))) * ((2 " ) * (a " ))
.= ((- b) - (sqrt (delta a,b,c))) * ((2 * a) " ) by XCMPLX_1:205 ;
hence y = ((- b) - (sqrt (delta a,b,c))) / (2 * a) by XCMPLX_0:def 9; :: thesis: verum

end;

((b ^2 ) - (4 * (a * c))) / 4 >= 0 / 4 by A2, A4, XREAL_1:74;
then ((a * y) + (b / 2)) ^2 = (sqrt (((b ^2 ) - (4 * (a * c))) / 4)) ^2 by A3, SQUARE_1:def 4;
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

end;

hence for x being real number holds
( not Polynom a,b,c,x = 0 or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) ) ; :: thesis: verum