scheme :: WELLFND1:sch 1
PFSeparation{ F₁() -> set , F₂() -> set , P₁[ set ] } :

ex PFS being Subset of (PFuncs (F₁(),F₂())) st
for pfs being PartFunc of F₁(),F₂() holds
( pfs in PFS iff P₁[pfs] )