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