for N being finite without_zero Subset of NAT ex k being Nat st N c= Seg k