theorem :: XREAL_1:231

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