theorem :: XREAL_1:230

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