let a, c, b be Real; :: thesis:
assume A1: ( a <> 0 & c / a < 0 ) ; :: thesis:

per cases by A1, XREAL_1:145;

case A2: ( c > 0 & a < 0 ) ; :: thesis:

then A3: 2 * a < 2 * 0 by XREAL_1:70;
4 * a < 4 * 0 by A2, XREAL_1:70;
then (4 * a) * c < 0 * c by A2, XREAL_1:70;
then A4: - ((4 * a) * c) > 0 by XREAL_1:60;
then (b ^2 ) + (- ((4 * a) * c)) > (b ^2 ) + 0 by XREAL_1:10;
then A5: sqrt ((b ^2 ) - ((4 * a) * c)) > sqrt (b ^2 ) by SQUARE_1:95, XREAL_1:65;
(- ((4 * a) * c)) + (b ^2 ) > 0 + 0 by A4, XREAL_1:10, XREAL_1:65;
then A6: - (- (sqrt ((b ^2 ) - ((4 * a) * c)))) > 0 by SQUARE_1:82, SQUARE_1:95;
then A7: - (sqrt ((b ^2 ) - ((4 * a) * c))) < 0 ;

per cases ;

suppose A8: b >= 0 ; :: thesis:

then - (- b) >= 0 ;
then A9: - b <= - 0 ;
sqrt ((b ^2 ) - ((4 * a) * c)) > b by A5, A8, SQUARE_1:89;
then (- b) + (sqrt ((b ^2 ) - ((4 * a) * c))) > (0 + b) + (- b) by XREAL_1:10;
then A10: ((- b) + (sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a) < 0 by A3, XREAL_1:144;
(- (sqrt ((b ^2 ) - ((4 * a) * c)))) + (- b) < 0 + 0 by A7, A9;
then (- b) - (sqrt ((b ^2 ) - ((4 * a) * c))) < 0 ;
then (- b) - (sqrt (delta a,b,c)) < 0 by QUIN_1:def 1;
hence ( ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) < 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 ) ) by A3, A10, QUIN_1:def 1, XREAL_1:142; :: thesis:

end;

suppose A11: b < 0 ; :: thesis:

then A12: - b > 0 by XREAL_1:60;
sqrt ((b ^2 ) - ((4 * a) * c)) > - b by A5, A11, SQUARE_1:90;
then - (- (b + (sqrt ((b ^2 ) - ((4 * a) * c))))) > 0 by XREAL_1:64;
then (- b) - (sqrt ((b ^2 ) - ((4 * a) * c))) < 0 ;
then A13: ((- b) - (sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a) > 0 by A3, XREAL_1:142;
(sqrt ((b ^2 ) - ((4 * a) * c))) + (- b) > 0 + 0 by A6, A12, XREAL_1:10;
then (sqrt (delta a,b,c)) + (- b) > 0 + 0 by QUIN_1:def 1;
hence ( ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) < 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 ) ) by A3, A13, QUIN_1:def 1, XREAL_1:144; :: thesis:

end;

hence ( ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) < 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 ) ) ; :: thesis:

end;

case A14: ( c < 0 & a > 0 ) ; :: thesis:

then A15: 2 * a > 0 by XREAL_1:131;
4 * a > 0 by A14, XREAL_1:131;
then (4 * a) * c < (4 * a) * 0 by A14, XREAL_1:70;
then A16: - ((4 * a) * c) > 0 by XREAL_1:60;
then (b ^2 ) + (- ((4 * a) * c)) > (b ^2 ) + 0 by XREAL_1:10;
then A17: sqrt ((b ^2 ) - ((4 * a) * c)) > sqrt (b ^2 ) by SQUARE_1:95, XREAL_1:65;
(- ((4 * a) * c)) + (b ^2 ) > 0 + 0 by A16, XREAL_1:10, XREAL_1:65;
then A18: - (- (sqrt ((b ^2 ) - ((4 * a) * c)))) > 0 by SQUARE_1:82, SQUARE_1:95;
then A19: - (sqrt ((b ^2 ) - ((4 * a) * c))) < 0 ;

per cases ;

suppose A20: b >= 0 ; :: thesis:

then - (- b) >= 0 ;
then A21: - b <= - 0 ;
sqrt ((b ^2 ) - ((4 * a) * c)) > b by A17, A20, SQUARE_1:89;
then (- b) + (sqrt ((b ^2 ) - ((4 * a) * c))) > (0 + b) + (- b) by XREAL_1:10;
then A22: ((- b) + (sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a) > 0 by A15, XREAL_1:141;
(- (sqrt ((b ^2 ) - ((4 * a) * c)))) + (- b) < 0 + 0 by A19, A21;
then (- b) - (sqrt ((b ^2 ) - ((4 * a) * c))) < 0 ;
then (- b) - (sqrt (delta a,b,c)) < 0 by QUIN_1:def 1;
hence ( ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) < 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 ) ) by A15, A22, QUIN_1:def 1, XREAL_1:143; :: thesis:

end;

suppose A23: b < 0 ; :: thesis:

then A24: - b > 0 by XREAL_1:60;
sqrt ((b ^2 ) - ((4 * a) * c)) > - b by A17, A23, SQUARE_1:90;
then - (- (b + (sqrt ((b ^2 ) - ((4 * a) * c))))) > 0 by XREAL_1:64;
then (- b) - (sqrt ((b ^2 ) - ((4 * a) * c))) < 0 ;
then A25: ((- b) - (sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a) < 0 by A15, XREAL_1:143;
(sqrt ((b ^2 ) - ((4 * a) * c))) + (- b) > 0 + 0 by A18, A24, XREAL_1:10;
then (sqrt (delta a,b,c)) + (- b) > 0 by QUIN_1:def 1;
hence ( ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) < 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 ) ) by A15, A25, QUIN_1:def 1, XREAL_1:141; :: thesis:

end;