theorem :: XREAL_1:8

for a, b, c, d being Real st a < b & c <= d holds
a + c < b + d by Lm8;