let a, b, c, d be Real; :: thesis: ( a < b & c <= d implies a + c < b + d )
assume that
A1: a < b and
A2: c <= d ; :: thesis: a + c < b + d
for a, b, c, d being Real st a < b & c <= d holds
a + c < b + d

proof

let a, b, c, d be Real; :: thesis: ( a < b & c <= d implies a + c < b + d )
assume A3: a < b ; :: thesis: ( not c <= d or a + c < b + d )
assume A4: c <= d ; :: thesis: a + c < b + d
A5: a + c <> b + d

proof

a + c <= d + a by A4, Lm5;
then (a + c) - d <= (a + d) - d by Lm7;
hence a + c <> b + d by A3; :: thesis: verum

end;

a + c <= b + d by A3, A4, Lm6;
hence a + c < b + d by A5, XXREAL_0:1; :: thesis: verum

end;

hence a + c < b + d by A1, A2; :: thesis: verum