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