for X being natural-membered set st ( for n being Nat holds n in X ) holds
X = NAT