theorem Th9: :: PYTHTRIP:9

for X being set st ( for m being Element of NAT ex n being Element of NAT st
( n >= m & n in X ) ) holds
X is infinite