theorem Th9: :: PYTHTRIP:9

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