let a, b, c, d be Real; :: thesis: ( a < b + c & b - c < d implies a - d < 2 * c )
assume that
A1: a < b + c and
A2: b - c < d ; :: thesis: a - d < 2 * c
a - d < (b + c) - (b - c) by A1, A2, XREAL_1:14;
hence a - d < 2 * c ; :: thesis: verum