theorem :: JORDAN5B:3

for i, k being Nat st 1 <= i & 1 <= k holds
(k -' i) + 1 <= k