let a, b, c be positive Real; :: thesis: ( a < b implies 1 < (b + c) / (a + c) )
assume a < b ; :: thesis: 1 < (b + c) / (a + c)
then a + c < b + c by XREAL_1:8;
hence 1 < (b + c) / (a + c) by XREAL_1:187; :: thesis: verum