theorem :: INT_1:4

for r being Real st r is Integer holds
( r + 1 is Integer & r - 1 is Integer ) ;