theorem :: XREAL_1:237

for a being Real st 1 <= a holds
a -' 1 < a