let a, b, c be positive Real; :: thesis: ( a > b & b > c implies b / (a - b) > c / (a - c) )
assume that
A1: a > b and
A2: b > c ; :: thesis: b / (a - b) > c / (a - c)
A3: a - b > 0 by A1, XREAL_1:50;
b * (- 1) < c * (- 1) by A2, XREAL_1:69;
then (- b) + a < (- c) + a by XREAL_1:8;
then A4: c / (a - b) > c / (a - c) by A3, XREAL_1:76;
b / (a - b) > c / (a - b) by A2, A3, XREAL_1:74;
hence b / (a - b) > c / (a - c) by A4, XXREAL_0:2; :: thesis: verum