for X being non empty ext-natural-membered set ex N being ExtNat st N in X