for k being Nat
for i1, i2 being Integer st i1 + k = i2 holds
i1 <= i2