theorem Th25: :: QUIN_1:25

for a, b, c being Real st a > 0 & delta (a,b,c) > 0 holds
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)