theorem :: XREAL_1:7

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