let p be Point of Niemytzki-plane; for r being positive Real 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 positive Real; 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 Real holds BB . |[x,0]| = { ((Ball (|[x,q]|,q)) \/ {|[x,0]|}) where q is Real : q > 0 }
and
A2:
for x, y being Real st y > 0 holds
BB . |[x,y]| = { ((Ball (|[x,y]|,q)) /\ y>=0-plane) where q is 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:53;
per cases
( p9 `2 = 0 or p9 `2 > 0 )
by A3, A4, Th18;
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 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:64;
then reconsider U =
(Ball (|[(p9 `1),(r / 2)]|,(r / 2))) \/ {p} as
open Subset of
Niemytzki-plane by A6, A4, A5, PRE_TOPC:def 2;
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 ZFMISC_1:136;
( 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:29;
a in Ball (
a,
(r / 2))
by Th13;
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 ZFMISC_1:136;
p9 - a = |[((p9 `1) - (p9 `1)),(0 - (r / 2))]|
by A4, A5, EUCLID:62;
then |.(p9 - a).| =
|.(0 - (r / 2)).|
by TOPREAL6:23
.=
|.((r / 2) - 0).|
by COMPLEX1:60
.=
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 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:64;
then reconsider U =
(Ball (p9,(r / 2))) /\ y>=0-plane as
open Subset of
Niemytzki-plane by A10, PRE_TOPC:def 2;
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 Th13;
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:29;
hence
|.(b - a).| < r
by A12, XXREAL_0:2;
verum end;