theorem Th1: :: NUMBER04:1

for X being non empty natural-membered set st ( for a being Nat st a in X holds
ex b being Nat st
( b > a & b in X ) ) holds
X is infinite