theorem :: SPPOL_1:1

for n, k being Nat st n < k holds
n <= k - 1