:: deftheorem Def1 defines ext-natural COUNTERS:def 2 :
for x being object holds
( x is ext-natural iff x in ExtNAT );