theorem :: INT_1:41

for r being Real holds
( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] )