theorem Th15: :: XREAL_1:15

for a, b, c, d being Real st a <= b & c < d holds
a - d < b - c