scheme :: MEMBERED:sch 3
RMSeparation{ P₁[ object ] } :

ex X being real-membered set st
for r being Real holds
( r in X iff P₁[r] )