theorem :: JORDAN5B:2

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