{ p where p is Point of (TOP-REAL 2) : ( P₁[p] & p <> 0. (TOP-REAL 2) ) } = { p7 where p7 is Point of (TOP-REAL 2) : P₁[p7] } /\ (NonZero (TOP-REAL 2))