theorem LM2: :: TOPMETR4:2

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