scheme :: GRAPH_1:sch 1
GraphSeparation{ F₁() -> Graph, P₁[ object ] } :

ex X being set st
for x being set holds
( x in X iff ( x is strict Subgraph of F₁() & P₁[x] ) )