:: deftheorem defines ext-natural-valued COUNTERS:def 11 :
for R being Relation holds
( R is ext-natural-valued iff rng R c= ExtNAT );