let a, b, c be real positive number ; :: thesis: ( a > b & b > c implies b / (a - b) > c / (a - c) )
assume A1: ( a > b & b > c ) ; :: thesis: b / (a - b) > c / (a - c)
then A2: ( a - b > 0 & b - c > 0 ) by XREAL_1:52;
then A3: b / (a - b) > c / (a - b) by A1, XREAL_1:76;
b * (- 1) < c * (- 1) by A1, XREAL_1:71;
then (- b) + a < (- c) + a by XREAL_1:10;
then c / (a - b) > c / (a - c) by A2, XREAL_1:78;
hence b / (a - b) > c / (a - c) by A3, XXREAL_0:2; :: thesis: verum