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