for X being Subset of NAT st X is infinite holds
ex N being increasing sequence of NAT st rng N c= X