for X being ext-natural-membered set st ( for N being ExtNat holds N in X ) holds
X = ExtNAT