theorem :: XREAL_1:147

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