theorem Th56: :: STIRL2_1:56

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