let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( P₁[p] & p <> 0.REAL 2 ) } or x in the carrier of (TOP-REAL 2) \ {(0.REAL 2)} )
assume x in { p where p is Point of (TOP-REAL 2) : ( P₁[p] & p <> 0.REAL 2 ) } ; :: thesis: x in the carrier of (TOP-REAL 2) \ {(0.REAL 2)}
then consider p8 being Point of (TOP-REAL 2) such that
A1: ( x = p8 & P₁[p8] & p8 <> 0.REAL 2 ) ;
not x in {(0.REAL 2)} by A1, TARSKI:def 1;
hence x in the carrier of (TOP-REAL 2) \ {(0.REAL 2)} by A1, XBOOLE_0:def 5; :: thesis: verum