theorem Th26: :: INT_1:26

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