theorem Th40: :: XREAL_1:40

for a, b, c being Real st 0 <= a & b < c holds
b < a + c