let a, b, c be positive Real; :: thesis: ( ((a + b) + c) / a > (a + b) / (a + c) & (a + b) / (a + c) > a / ((a + b) + c) )
reconsider k = (a + b) / a as positive heavy Real ;
A1: a + b = k * a by XCMPLX_1:87;
reconsider l = (a + c) / a as positive heavy Real ;
A2: a + c = l * a by XCMPLX_1:87;
A3: k / l = (a + b) / (a + c) by XCMPLX_1:55;
A4: ( (k + l) - 1 > k / l & k / l > 1 / ((k + l) - 1) ) by ADB;
(a + b) + c = ((k + l) - 1) * a by A1, A2;
then ((a + b) + c) / a = (k + l) - 1 by XCMPLX_1:89;
hence ( ((a + b) + c) / a > (a + b) / (a + c) & (a + b) / (a + c) > a / ((a + b) + c) ) by A3, A4, XCMPLX_1:213; :: thesis: verum