theorem :: MEMBERED:18

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