theorem :: XREAL_1:146

for a being Real holds a - 1 < a