for k being Integer st 1 <= k holds
k is Nat