theorem :: NAT_D:47

for i1, i2 being natural Number st ( i1 + 2 <= i2 or (i1 + 1) + 1 <= i2 ) holds
( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 & (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )