theorem Th40: :: SEQM_3:41

for r, s being Real holds
( |.(r - s).| = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) )