let p be Point of Niemytzki-plane; :: thesis: 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; :: thesis: 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 ; :: thesis: 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)]|; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r
let b be Point of (TOP-REAL 2); :: thesis: ( b in U implies |.(b - a).| < r )
assume b in U ; :: thesis: |.(b - a).| < r
then 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; :: thesis: verum

end;

suppose A9: p9 `2 > 0 ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: for b being Point of (TOP-REAL 2) st b in U holds
|.(b - a).| < r
let b be Point of (TOP-REAL 2); :: thesis: ( b in U implies |.(b - a).| < r )
assume b in U ; :: thesis: |.(b - a).| < r
then 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; :: thesis: verum

end;

end;