scheme :: MEMBERED:sch 6
NMSeparation{ P1[ object ] } :
ex X being natural-membered set st
for n being Nat holds
( n in X iff P1[n] )