let a, b be positive heavy Real; :: thesis: ( (a + b) - 1 > a / b & a / b > 1 / ((a + b) - 1) )
( a > 1 & b > 1 ) by TA1;
then a + b > 1 + 1 by XREAL_1:8;
then (a + b) - 1 > 2 - 1 by XREAL_1:9;
then reconsider c = (a + b) - 1 as positive heavy Real by TA1;
reconsider k = a / b as positive Real ;
(k + 1) * b > (k + 1) * 1 by TA1, XREAL_1:68;
then ((k + 1) * b) - 1 > (k + 1) - 1 by XREAL_1:9;
then A1: ((k * b) + b) - 1 > k ;
((k ") + 1) * a > ((k ") + 1) * 1 by TA1, XREAL_1:68;
then (((k ") + 1) * a) - 1 > ((k ") + 1) - 1 by XREAL_1:9;
then (((k ") * a) + a) - 1 > k " ;
then (((b / a) * a) + a) - 1 > k " by XCMPLX_1:213;
then (((b + a) - 1) ") " > k " by XCMPLX_1:87;
hence ( (a + b) - 1 > a / b & a / b > 1 / ((a + b) - 1) ) by A1, XCMPLX_1:87, XREAL_1:91; :: thesis: verum