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