theorem :: XREAL_1:145

for a, b being Real st a <= b holds
a < b + 1