let a, b, c, d be real number ; :: thesis: ( a < b & c <= d implies a + c < b + d )
assume A1: ( a < b & c <= d ) ; :: thesis: a + c < b + d
for a, b, c, d being real number st a < b & c <= d holds
a + c < b + d

proof

let a, b, c, d be real number ; :: thesis: ( a < b & c <= d implies a + c < b + d )
assume A2: a < b ; :: thesis: ( not c <= d or a + c < b + d )
assume A3: c <= d ; :: thesis: a + c < b + d
then A4: a + c <= b + d by A2, Lm6;
a + c <> b + d

proof

assume A5: a + c = b + d ; :: thesis: contradiction
b <= a

proof

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

end;

hence contradiction by A2; :: thesis: verum

end;

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

end;

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