let a, b, c be Real; :: thesis: ( not c / a < 0 or ( ((- 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 ) )
assume A1: c / a < 0 ; :: thesis: ( ( ((- 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 ) )

now :: thesis: ( ( c > 0 & a < 0 & ( ( ((- 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 ) ) ) or ( c < 0 & a > 0 & ( ( ((- 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 ) ) ) )

per cases ( ( c > 0 & a < 0 ) or ( c < 0 & a > 0 ) ) by A1, XREAL_1:143;

case A2: ( c > 0 & a < 0 ) ; :: thesis: ( ( ((- 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 ) )

then 4 * a < 4 * 0 by XREAL_1:68;
then (4 * a) * c < 0 * c by A2, XREAL_1:68;
then A3: - ((4 * a) * c) > 0 by XREAL_1:58;
then (b ^2) + (- ((4 * a) * c)) > (b ^2) + 0 by XREAL_1:8;
then A4: sqrt ((b ^2) - ((4 * a) * c)) > sqrt (b ^2) by SQUARE_1:27, XREAL_1:63;
A5: 2 * a < 2 * 0 by A2, XREAL_1:68;
(- ((4 * a) * c)) + (b ^2) > 0 + 0 by A3, XREAL_1:8, XREAL_1:63;
then A6: - (- (sqrt ((b ^2) - ((4 * a) * c)))) > 0 by SQUARE_1:17, SQUARE_1:27;
then A7: - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ;

now :: thesis: ( ( ((- 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 ) )

per cases ( b >= 0 or b < 0 ) ;

suppose A8: b >= 0 ; :: thesis: ( ( ((- 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 ) )

then - b <= - 0 ;
then (- (sqrt ((b ^2) - ((4 * a) * c)))) + (- b) < 0 + 0 by A7;
then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ;
then A9: (- b) - (sqrt (delta (a,b,c))) < 0 by QUIN_1:def 1;
sqrt ((b ^2) - ((4 * a) * c)) > b by A4, A8, SQUARE_1:22;
then (- b) + (sqrt ((b ^2) - ((4 * a) * c))) > (0 + b) + (- b) by XREAL_1:8;
then ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0 by A5, XREAL_1:142;
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 A5, A9, QUIN_1:def 1, XREAL_1:140; :: thesis: verum

end;

suppose A10: b < 0 ; :: thesis: ( ( ((- 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 ) )

then sqrt ((b ^2) - ((4 * a) * c)) > - b by A4, SQUARE_1:23;
then - (- (b + (sqrt ((b ^2) - ((4 * a) * c))))) > 0 by XREAL_1:62;
then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ;
then A11: ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A5, XREAL_1:140;
- b > 0 by A10, XREAL_1:58;
then (sqrt ((b ^2) - ((4 * a) * c))) + (- b) > 0 + 0 by A6;
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 A5, A11, QUIN_1:def 1, XREAL_1:142; :: thesis: verum

end;

end;

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: verum

end;

case A12: ( c < 0 & a > 0 ) ; :: thesis: ( ( ((- 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 ) )

then 4 * a > 0 by XREAL_1:129;
then (4 * a) * c < (4 * a) * 0 by A12, XREAL_1:68;
then A13: - ((4 * a) * c) > 0 by XREAL_1:58;
then (b ^2) + (- ((4 * a) * c)) > (b ^2) + 0 by XREAL_1:8;
then A14: sqrt ((b ^2) - ((4 * a) * c)) > sqrt (b ^2) by SQUARE_1:27, XREAL_1:63;
A15: 2 * a > 0 by A12, XREAL_1:129;
(- ((4 * a) * c)) + (b ^2) > 0 + 0 by A13, XREAL_1:8, XREAL_1:63;
then A16: - (- (sqrt ((b ^2) - ((4 * a) * c)))) > 0 by SQUARE_1:17, SQUARE_1:27;
then A17: - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ;

now :: thesis: ( ( ((- 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 ) )

per cases ( b >= 0 or b < 0 ) ;

suppose A18: b >= 0 ; :: thesis: ( ( ((- 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 ) )

then - b <= - 0 ;
then (- (sqrt ((b ^2) - ((4 * a) * c)))) + (- b) < 0 + 0 by A17;
then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ;
then A19: (- b) - (sqrt (delta (a,b,c))) < 0 by QUIN_1:def 1;
sqrt ((b ^2) - ((4 * a) * c)) > b by A14, A18, SQUARE_1:22;
then (- b) + (sqrt ((b ^2) - ((4 * a) * c))) > (0 + b) + (- b) by XREAL_1:8;
then ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A15, XREAL_1:139;
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 A12, A19, QUIN_1:def 1, XREAL_1:129, XREAL_1:141; :: thesis: verum

end;

suppose A20: b < 0 ; :: thesis: ( ( ((- 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 ) )

then sqrt ((b ^2) - ((4 * a) * c)) > - b by A14, SQUARE_1:23;
then - (- (b + (sqrt ((b ^2) - ((4 * a) * c))))) > 0 by XREAL_1:62;
then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ;
then A21: ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0 by A12, XREAL_1:129, XREAL_1:141;
- b > 0 by A20, XREAL_1:58;
then (sqrt ((b ^2) - ((4 * a) * c))) + (- b) > 0 + 0 by A16;
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, A21, QUIN_1:def 1, XREAL_1:139; :: thesis: verum

end;

end;

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: verum

end;

end;

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: verum