:: deftheorem Def2 defines ext-natural-membered COUNTERS:def 3 :
for X being set holds
( X is ext-natural-membered iff for x being object st x in X holds
x is ext-natural );