scheme :: JGRAPH_2:sch 2
TopCompl{ P₁[ set ], F₁() -> Subset of (TOP-REAL 2) } :

F₁() ` = { p where p is Point of (TOP-REAL 2) : P₁[p] }

provided

A1: F₁() = { p where p is Point of (TOP-REAL 2) : P₁[p] }