set B0 = NonZero (TOP-REAL 2);

set K1 = { p7 where p7 is Point of (TOP-REAL 2) : P_{1}[p7] } ;

set K0 = { p where p is Point of (TOP-REAL 2) : ( P_{1}[p] & p <> 0. (TOP-REAL 2) ) } ;

A1: { p7 where p7 is Point of (TOP-REAL 2) : P_{1}[p7] } /\ (NonZero (TOP-REAL 2)) c= { p where p is Point of (TOP-REAL 2) : ( P_{1}[p] & p <> 0. (TOP-REAL 2) ) }
_{1}[p] & p <> 0. (TOP-REAL 2) ) } c= { p7 where p7 is Point of (TOP-REAL 2) : P_{1}[p7] } /\ (NonZero (TOP-REAL 2))
_{1}[p] & p <> 0. (TOP-REAL 2) ) } = { p7 where p7 is Point of (TOP-REAL 2) : P_{1}[p7] } /\ (NonZero (TOP-REAL 2))
by A1; :: thesis: verum

set K1 = { p7 where p7 is Point of (TOP-REAL 2) : P

set K0 = { p where p is Point of (TOP-REAL 2) : ( P

A1: { p7 where p7 is Point of (TOP-REAL 2) : P

proof

{ p where p is Point of (TOP-REAL 2) : ( P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p7 where p7 is Point of (TOP-REAL 2) : P_{1}[p7] } /\ (NonZero (TOP-REAL 2)) or x in { p where p is Point of (TOP-REAL 2) : ( P_{1}[p] & p <> 0. (TOP-REAL 2) ) } )

assume A2: x in { p7 where p7 is Point of (TOP-REAL 2) : P_{1}[p7] } /\ (NonZero (TOP-REAL 2))
; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( P_{1}[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_{1}[p7] }
by A2, XBOOLE_0:def 4;

then ex p7 being Point of (TOP-REAL 2) st

( p7 = x & P_{1}[p7] )
;

hence x in { p where p is Point of (TOP-REAL 2) : ( P_{1}[p] & p <> 0. (TOP-REAL 2) ) }
by A3; :: thesis: verum

end;assume A2: x in { p7 where p7 is Point of (TOP-REAL 2) : P

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

then ex p7 being Point of (TOP-REAL 2) st

( p7 = x & P

hence x in { p where p is Point of (TOP-REAL 2) : ( P

proof

hence
{ p where p is Point of (TOP-REAL 2) : ( P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( P_{1}[p] & p <> 0. (TOP-REAL 2) ) } or x in { p7 where p7 is Point of (TOP-REAL 2) : P_{1}[p7] } /\ (NonZero (TOP-REAL 2)) )

assume x in { p where p is Point of (TOP-REAL 2) : ( P_{1}[p] & p <> 0. (TOP-REAL 2) ) }
; :: thesis: x in { p7 where p7 is Point of (TOP-REAL 2) : P_{1}[p7] } /\ (NonZero (TOP-REAL 2))

then A4: ex p being Point of (TOP-REAL 2) st

( x = p & P_{1}[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_{1}[p7] }
by A4;

hence x in { p7 where p7 is Point of (TOP-REAL 2) : P_{1}[p7] } /\ (NonZero (TOP-REAL 2))
by A5, XBOOLE_0:def 4; :: thesis: verum

end;assume x in { p where p is Point of (TOP-REAL 2) : ( P

then A4: ex p being Point of (TOP-REAL 2) st

( x = p & P

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

hence x in { p7 where p7 is Point of (TOP-REAL 2) : P