scheme :: COUNTERS:sch 1
ENMSeparation{ P₁[ object ] } :

ex X being ext-natural-membered set st
for N being ExtNat holds
( N in X iff P₁[N] )