scheme :: MEMBERED:sch 6
NMSeparation{ P₁[ object ] } :

ex X being natural-membered set st
for n being Nat holds
( n in X iff P₁[n] )