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

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