let a, b, c be Real; ( a > 0 & delta (a,b,c) > 0 implies ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) )
assume that
A1:
a > 0
and
A2:
delta (a,b,c) > 0
; ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)
sqrt (delta (a,b,c)) > 0
by A2, SQUARE_1:25;
then
2 * (sqrt (delta (a,b,c))) > 0
by XREAL_1:129;
then
(sqrt (delta (a,b,c))) + (sqrt (delta (a,b,c))) > 0
;
then
sqrt (delta (a,b,c)) > - (sqrt (delta (a,b,c)))
by XREAL_1:59;
then A3:
(- b) + (sqrt (delta (a,b,c))) > (- b) + (- (sqrt (delta (a,b,c))))
by XREAL_1:6;
2 * a > 0
by A1, XREAL_1:129;
hence
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)
by A3, XREAL_1:74; verum