let a, b, c be real positive number ; :: 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:10;
hence 1 < (b + c) / (a + c) by XREAL_1:189; :: thesis: verum