scheme :: MEMBERED:sch 2
EMSeparation{ P₁[ object ] } :

ex X being ext-real-membered set st
for e being ExtReal holds
( e in X iff P₁[e] )