theorem :: INT_1:32

for r being Real holds
( r - 1 < [/r\] & r < [/r\] + 1 )