scheme :: TOPREAL1:sch 2
TRSubsetEx{ F₁() -> Nat, P₁[ object ] } :

ex A being Subset of (TOP-REAL F₁()) st
for p being Point of (TOP-REAL F₁()) holds
( p in A iff P₁[p] )