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