let a, b, c be Real; :: thesis: ( b / a < 0 & c / a > 0 & delta (a,b,c) >= 0 implies ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
assume that
A1: b / a < 0 and
A2: c / a > 0 and
A3: delta (a,b,c) >= 0 ; :: thesis: ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 )
A4: (b ^2) - ((4 * a) * c) >= 0 by A3, QUIN_1:def 1;

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

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

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

A6: 0 <= sqrt ((b ^2) - ((4 * a) * c)) by A4, SQUARE_1:17, SQUARE_1:26;
A7: 2 * a > 0 by A5, XREAL_1:129;
- b > 0 by A5, XREAL_1:58;
then (- b) + (sqrt ((b ^2) - ((4 * a) * c))) > 0 + 0 by A6;
then A8: ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A7, XREAL_1:139;
( c > 0 & 4 * a > 0 ) by A2, A5, XREAL_1:129;
then - (- ((4 * a) * c)) > 0 by XREAL_1:129;
then - ((4 * a) * c) < 0 ;
then (b ^2) + (- ((4 * a) * c)) < (b ^2) + 0 by XREAL_1:8;
then sqrt ((b ^2) - ((4 * a) * c)) < sqrt (b ^2) by A4, SQUARE_1:27;
then sqrt ((b ^2) - ((4 * a) * c)) < - b by A5, SQUARE_1:23;
then - (sqrt ((b ^2) - ((4 * a) * c))) > - (- b) by XREAL_1:24;
then (- (sqrt ((b ^2) - ((4 * a) * c)))) + (- b) > (- (- b)) + (- b) by XREAL_1:8;
then ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A7, XREAL_1:139;
hence ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) by A8, QUIN_1:def 1; :: thesis: verum

end;

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

then A10: a * 2 < 0 * 2 by XREAL_1:68;
c < 0 by A2, A9;
then a * c > 0 by A9, XREAL_1:130;
then 4 * (a * c) > 0 by XREAL_1:129;
then - (- ((4 * a) * c)) > 0 ;
then - ((4 * a) * c) < 0 ;
then (b ^2) + (- ((4 * a) * c)) < (b ^2) + 0 by XREAL_1:8;
then sqrt ((b ^2) - ((4 * a) * c)) < sqrt (b ^2) by A4, SQUARE_1:27;
then sqrt ((b ^2) - ((4 * a) * c)) < b by A9, SQUARE_1:22;
then (- b) + (sqrt ((b ^2) - ((4 * a) * c))) < (0 + b) + (- b) by XREAL_1:8;
then A11: ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A10, XREAL_1:140;
A12: 0 <= sqrt ((b ^2) - ((4 * a) * c)) by A4, SQUARE_1:17, SQUARE_1:26;
- (- b) > 0 by A9;
then (- b) + 0 < 0 + (sqrt ((b ^2) - ((4 * a) * c))) by A12;
then - (- ((sqrt ((b ^2) - ((4 * a) * c))) + b)) > 0 by XREAL_1:62;
then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ;
then ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A10, XREAL_1:140;
hence ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) by A11, QUIN_1:def 1; :: thesis: verum

end;

end;

end;

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