let a, b, c be Real; :: thesis: ( a <> 0 & 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 A1: ( a <> 0 & b / a < 0 & c / a > 0 & delta a,b,c >= 0 ) ; :: thesis: ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 )
then A2: (b ^2 ) - ((4 * a) * c) >= 0 by QUIN_1:def 1;

now

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

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

then A4: 2 * a > 0 by XREAL_1:131;
A5: - b > 0 by A3, XREAL_1:60;
A6: c > 0 by A1, A3, XREAL_1:146;
0 <= sqrt ((b ^2 ) - ((4 * a) * c)) by A2, SQUARE_1:82, SQUARE_1:94;
then (- b) + (sqrt ((b ^2 ) - ((4 * a) * c))) > 0 + 0 by A5, XREAL_1:10;
then A7: ((- b) + (sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a) > 0 by A4, XREAL_1:141;
4 * a > 0 by A3, XREAL_1:131;
then - (- ((4 * a) * c)) > 0 by A6, XREAL_1:131;
then - ((4 * a) * c) < 0 ;
then (b ^2 ) + (- ((4 * a) * c)) < (b ^2 ) + 0 by XREAL_1:10;
then sqrt ((b ^2 ) - ((4 * a) * c)) < sqrt (b ^2 ) by A2, SQUARE_1:95;
then sqrt ((b ^2 ) - ((4 * a) * c)) < - b by A3, SQUARE_1:90;
then - (sqrt ((b ^2 ) - ((4 * a) * c))) > - (- b) by XREAL_1:26;
then (- (sqrt ((b ^2 ) - ((4 * a) * c)))) + (- b) > (- (- b)) + (- b) by XREAL_1:10;
then ((- b) - (sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a) > 0 by A4, XREAL_1:141;
hence ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 ) by A7, QUIN_1:def 1; :: thesis: verum

end;

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

then A9: a * 2 < 0 * 2 by XREAL_1:70;
- (- b) > 0 by A8;
then A10: - b < 0 ;
A11: c < 0 by A1, A8, XREAL_1:146;
0 <= sqrt ((b ^2 ) - ((4 * a) * c)) by A2, SQUARE_1:82, SQUARE_1:94;
then (- b) + 0 < 0 + (sqrt ((b ^2 ) - ((4 * a) * c))) by A10, XREAL_1:10;
then - (- ((sqrt ((b ^2 ) - ((4 * a) * c))) + b)) > 0 by XREAL_1:64;
then (- b) - (sqrt ((b ^2 ) - ((4 * a) * c))) < 0 ;
then A12: ((- b) - (sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a) > 0 by A9, XREAL_1:142;
a * c > 0 by A8, A11, XREAL_1:132;
then 4 * (a * c) > 0 by XREAL_1:131;
then - (- ((4 * a) * c)) > 0 ;
then - ((4 * a) * c) < 0 ;
then (b ^2 ) + (- ((4 * a) * c)) < (b ^2 ) + 0 by XREAL_1:10;
then sqrt ((b ^2 ) - ((4 * a) * c)) < sqrt (b ^2 ) by A2, SQUARE_1:95;
then sqrt ((b ^2 ) - ((4 * a) * c)) < b by A8, SQUARE_1:89;
then (- b) + (sqrt ((b ^2 ) - ((4 * a) * c))) < (0 + b) + (- b) by XREAL_1:10;
then ((- b) + (sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a) > 0 by A9, XREAL_1:142;
hence ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 ) by A12, 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