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