let p be Point of Niemytzki-plane ; for r being real positive number ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )
let r be real positive number ; ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )
consider BB being Neighborhood_System of Niemytzki-plane such that
A1:
for x being Element of REAL holds BB . |[x,0 ]| = { ((Ball |[x,q]|,q) \/ {|[x,0 ]|}) where q is Element of REAL : q > 0 }
and
A2:
for x, y being Element of REAL st y > 0 holds
BB . |[x,y]| = { ((Ball |[x,y]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 }
by Def3;
A3:
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
p in the carrier of Niemytzki-plane
;
then reconsider p9 = p as Point of (TOP-REAL 2) by A3;
A4:
p = |[(p9 `1 ),(p9 `2 )]|
by EUCLID:57;
per cases
( p9 `2 = 0 or p9 `2 > 0 )
by A3, A4, Th22;
suppose A5:
p9 `2 = 0
;
ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )then
BB . p = { ((Ball |[(p9 `1 ),q]|,q) \/ {|[(p9 `1 ),0 ]|}) where q is Element of REAL : q > 0 }
by A1, A4;
then A6:
(Ball |[(p9 `1 ),(r / 2)]|,(r / 2)) \/ {|[(p9 `1 ),0 ]|} in BB . p
;
BB . p c= the
topology of
Niemytzki-plane
by TOPS_2:78;
then reconsider U =
(Ball |[(p9 `1 ),(r / 2)]|,(r / 2)) \/ {p} as
open Subset of
Niemytzki-plane by A6, A4, A5, PRE_TOPC:def 5;
take a =
|[(p9 `1 ),(r / 2)]|;
ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )take
U
;
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )thus
p in U
by SETWISEO:6;
( a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )A7:
r / 2
< (r / 2) + (r / 2)
by XREAL_1:31;
a in Ball a,
(r / 2)
by Th17;
hence
a in U
by XBOOLE_0:def 3;
for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < rlet b be
Point of
(TOP-REAL 2);
( b in U implies |.(b - a).| < r )assume
b in U
;
|.(b - a).| < rthen A8:
(
b in Ball a,
(r / 2) or
b = p )
by SETWISEO:6;
p9 - a = |[((p9 `1 ) - (p9 `1 )),(0 - (r / 2))]|
by A4, A5, EUCLID:66;
then |.(p9 - a).| =
|.(0 - (r / 2)).|
by TOPREAL6:31
.=
|.((r / 2) - 0 ).|
by COMPLEX1:146
.=
r / 2
by ABSVALUE:def 1
;
then
|.(b - a).| <= r / 2
by A8, TOPREAL9:7;
hence
|.(b - a).| < r
by A7, XXREAL_0:2;
verum end; suppose A9:
p9 `2 > 0
;
ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )then
BB . p = { ((Ball |[(p9 `1 ),(p9 `2 )]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 }
by A2, A4;
then A10:
(Ball p9,(r / 2)) /\ y>=0-plane in BB . p
by A4;
BB . p c= the
topology of
Niemytzki-plane
by TOPS_2:78;
then reconsider U =
(Ball p9,(r / 2)) /\ y>=0-plane as
open Subset of
Niemytzki-plane by A10, PRE_TOPC:def 5;
take a =
p9;
ex U being open Subset of Niemytzki-plane st
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )take
U
;
( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r ) )A11:
p in Ball a,
(r / 2)
by Th17;
p in y>=0-plane
by A4, A9;
hence
(
p in U &
a in U )
by A11, XBOOLE_0:def 4;
for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < rlet b be
Point of
(TOP-REAL 2);
( b in U implies |.(b - a).| < r )assume
b in U
;
|.(b - a).| < rthen
b in Ball a,
(r / 2)
by XBOOLE_0:def 4;
then A12:
|.(b - a).| <= r / 2
by TOPREAL9:7;
r / 2
< (r / 2) + (r / 2)
by XREAL_1:31;
hence
|.(b - a).| < r
by A12, XXREAL_0:2;
verum end;