let a, b, c be positive Real; :: thesis: ((a + b) + c) / (a + b) < (a + c) / a
(a + b) * (a + c) > ((a + b) + c) * a by FPC;
hence ((a + b) + c) / (a + b) < (a + c) / a by XREAL_1:106; :: thesis: verum