theorem Th35: :: INT_1:35

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