theorem INT17: :: NUMERAL3:2

for a, b being Integer holds
( ( a <= b & b <= a + 1 ) iff ( b = a or b = a + 1 ) )