for A being Subset of REAL st 0 in A & ( for x being Real st x in A holds
x + 1 in A ) holds
NAT c= A