let a, b, c, d be Real; :: thesis: ( a <= b + c & b <= d implies a <= d + c )
assume A1: ( a <= b + c & b <= d ) ; :: thesis: a <= d + c
then b + c <= d + c by XREAL_1:7;
hence a <= d + c by A1, XXREAL_0:2; :: thesis: verum