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