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

proof

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

end;

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

proof

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. (TOP-REAL 2) ) } or x in { p7 where p7 is Point of (TOP-REAL 2) : P₁[p7] } /\ (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 { p7 where p7 is Point of (TOP-REAL 2) : P₁[p7] } /\ (NonZero (TOP-REAL 2))
then A4: ex p being Point of (TOP-REAL 2) st
( x = p & P₁[p] & p <> 0. (TOP-REAL 2) ) ;
then not x in {(0. (TOP-REAL 2))} by TARSKI:def 1;
then A5: x in NonZero (TOP-REAL 2) by A4, XBOOLE_0:def 5;
x in { p7 where p7 is Point of (TOP-REAL 2) : P₁[p7] } by A4;
hence x in { p7 where p7 is Point of (TOP-REAL 2) : P₁[p7] } /\ (NonZero (TOP-REAL 2)) by A5, XBOOLE_0:def 4; :: thesis: verum

end;

hence { 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)) by A1, XBOOLE_0:def 10; :: thesis: verum