theorem Th31: :: INT_1:31

for r being Real holds
( r < [/r\] iff not r is integer )