theorem Th1: :: NAT_1:1

for X being Subset of REAL st 0 in X & ( for x being Real st x in X holds
x + 1 in X ) holds
for n being Nat holds n in X