consider BB being Neighborhood_System of Niemytzki-plane such that
A1:
for x being Element of REAL holds BB . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Element of REAL : r > 0 }
and
for x, y being Element of REAL st y > 0 holds
BB . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Element of REAL : r > 0 }
by Def3;
let A be Subset of Niemytzki-plane; ( A = y=0-line implies Der A is empty )
assume that
A2:
A = y=0-line
and
A3:
not Der A is empty
; contradiction
consider a being Element of Der A;
a in Der A
by A3;
then reconsider a = a as Point of Niemytzki-plane ;
A4:
a in Der A
by A3;
a is_an_accumulation_point_of A
by A3, TOPGEN_1:def 3;
then A5:
a in Cl (A \ {a})
by TOPGEN_1:def 2;
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
then
a in y>=0-plane
;
then reconsider b = a as Point of (TOP-REAL 2) ;
A6:
a = |[(b `1),(b `2)]|
by EUCLID:57;
A7:
Der A c= Cl A
by TOPGEN_1:30;
Cl A = A
by A2, Th39;
then A8:
b `2 = 0
by A4, A7, A2, A6, Th19;
then
BB . a = { ((Ball (|[(b `1),r]|,r)) \/ {|[(b `1),0]|}) where r is Element of REAL : r > 0 }
by A1, A6;
then
(Ball (|[(b `1),1]|,1)) \/ {b} in BB . a
by A6, A8;
then
(Ball (|[(b `1),1]|,1)) \/ {b} meets A \ {a}
by A5, TOPGEN_2:10;
then consider z being set such that
A9:
z in (Ball (|[(b `1),1]|,1)) \/ {b}
and
A10:
z in A \ {a}
by XBOOLE_0:3;
A11:
z in A
by A10, ZFMISC_1:64;
z <> a
by A10, ZFMISC_1:64;
then A12:
z in Ball (|[(b `1),1]|,1)
by A9, SETWISEO:6;
reconsider z = z as Point of (TOP-REAL 2) by A9;
A13:
z = |[(z `1),(z `2)]|
by EUCLID:57;
then
z `2 = 0
by A2, A11, Th19;
then A14:
z - |[(b `1),1]| = |[((z `1) - (b `1)),(0 - 1)]|
by A13, EUCLID:66;
A15:
|[((z `1) - (b `1)),(0 - 1)]| `2 = 0 - 1
by EUCLID:56;
|[((z `1) - (b `1)),(0 - 1)]| `1 = (z `1) - (b `1)
by EUCLID:56;
then |.(z - |[(b `1),1]|).| =
sqrt ((((z `1) - (b `1)) ^2) + ((- 1) ^2))
by A14, A15, JGRAPH_1:47
.=
sqrt ((((z `1) - (b `1)) ^2) + (1 ^2))
;
then A16:
|.(z - |[(b `1),1]|).| >= abs 1
by COMPLEX1:165;
|.(z - |[(b `1),1]|).| < 1
by A12, TOPREAL9:7;
then
abs 1 < 1
by A16, XXREAL_0:2;
hence
contradiction
by ABSVALUE:11; verum