for X being non empty natural-membered set ex n being Nat st n in X