for N being Subset of NAT st N is finite holds
ex k being Nat st
for n being Nat st n in N holds
n <= k