let A be Subset of Niemytzki-plane; ( A = (y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) implies for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane )
assume A1:
A = (y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>)
; for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane
let s be set ; Cl (A \ {s}) = [#] Niemytzki-plane
thus
Cl (A \ {s}) c= [#] Niemytzki-plane
; XBOOLE_0:def 10 [#] Niemytzki-plane c= Cl (A \ {s})
let x be object ; TARSKI:def 3 ( not x in [#] Niemytzki-plane or x in Cl (A \ {s}) )
assume
x in [#] Niemytzki-plane
; x in Cl (A \ {s})
then reconsider a = x as Element of Niemytzki-plane ;
reconsider b = a as Element of y>=0-plane by Def3;
consider BB being Neighborhood_System of Niemytzki-plane such that
A2:
for x being Real holds BB . |[x,0]| = { ((Ball (|[x,q]|,q)) \/ {|[x,0]|}) where q is Real : q > 0 }
and
A3:
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;
A4:
a = |[(b `1),(b `2)]|
by EUCLID:53;
for U being set st U in BB . a holds
U meets A \ {s}
proof
let U be
set ;
( U in BB . a implies U meets A \ {s} )
assume A5:
U in BB . a
;
U meets A \ {s}
per cases
( b `2 = 0 or b `2 > 0 )
by A4, Th18;
suppose A6:
b `2 = 0
;
U meets A \ {s}then
BB . a = { ((Ball (|[(b `1),q]|,q)) \/ {|[(b `1),0]|}) where q is Real : q > 0 }
by A2, A4;
then consider q being
Real such that A7:
U = (Ball (|[(b `1),q]|,q)) \/ {a}
and A8:
q > 0
by A4, A5, A6;
reconsider q =
q as
positive Real by A8;
consider w1,
v1 being
Rational such that A9:
|[w1,v1]| in Ball (
|[(b `1),q]|,
q)
and A10:
|[w1,v1]| <> |[(b `1),q]|
by Th31;
A11:
|[w1,v1]| in U
by A7, A9, XBOOLE_0:def 3;
set q2 =
|.(|[w1,v1]| - |[(b `1),q]|).|;
|[w1,v1]| - |[(b `1),q]| <> 0. (TOP-REAL 2)
by A10, RLVECT_1:21;
then
|.(|[w1,v1]| - |[(b `1),q]|).| <> 0
by EUCLID_2:42;
then reconsider q2 =
|.(|[w1,v1]| - |[(b `1),q]|).| as
positive Real ;
A12:
q2 < q
by A9, TOPREAL9:7;
consider w2,
v2 being
Rational such that A13:
|[w2,v2]| in Ball (
|[(b `1),q]|,
q2)
and
|[w2,v2]| <> |[(b `1),q]|
by Th31;
|.(|[w2,v2]| - |[(b `1),q]|).| < q2
by A13, TOPREAL9:7;
then
|.(|[w2,v2]| - |[(b `1),q]|).| < q
by A12, XXREAL_0:2;
then A14:
|[w2,v2]| in Ball (
|[(b `1),q]|,
q)
by TOPREAL9:7;
then A15:
|[w2,v2]| in U
by A7, XBOOLE_0:def 3;
A16:
Ball (
|[(b `1),q]|,
q)
misses y=0-line
by Th21;
Ball (
|[(b `1),q]|,
q)
c= y>=0-plane
by Th20;
then A17:
Ball (
|[(b `1),q]|,
q)
c= y>=0-plane \ y=0-line
by A16, XBOOLE_1:86;
A18:
v1 in RAT
by RAT_1:def 2;
w1 in RAT
by RAT_1:def 2;
then
|[w1,v1]| in product <*RAT,RAT*>
by A18, FINSEQ_3:124;
then A19:
|[w1,v1]| in A
by A17, A9, A1, XBOOLE_0:def 4;
A20:
(
s = |[w1,v1]| or
s <> |[w1,v1]| )
;
A21:
v2 in RAT
by RAT_1:def 2;
w2 in RAT
by RAT_1:def 2;
then
|[w2,v2]| in product <*RAT,RAT*>
by A21, FINSEQ_3:124;
then A22:
|[w2,v2]| in A
by A17, A14, A1, XBOOLE_0:def 4;
|[w2,v2]| <> |[w1,v1]|
by A13, TOPREAL9:7;
then
(
|[w1,v1]| in A \ {s} or
|[w2,v2]| in A \ {s} )
by A20, A19, A22, ZFMISC_1:56;
hence
U meets A \ {s}
by A11, A15, XBOOLE_0:3;
verum end; suppose A23:
b `2 > 0
;
U meets A \ {s}then
BB . a = { ((Ball (|[(b `1),(b `2)]|,q)) /\ y>=0-plane) where q is Real : q > 0 }
by A3, A4;
then consider q being
Real such that A24:
U = (Ball (b,q)) /\ y>=0-plane
and A25:
q > 0
by A4, A5;
reconsider q =
q,
b2 =
b `2 as
positive Real by A23, A25;
reconsider q1 =
min (
q,
b2) as
positive Real by XXREAL_0:def 9;
consider w1,
v1 being
Rational such that A26:
|[w1,v1]| in Ball (
b,
q1)
and A27:
|[w1,v1]| <> b
by A4, Th31;
A28:
v1 in RAT
by RAT_1:def 2;
set q2 =
|.(|[w1,v1]| - b).|;
|[w1,v1]| - b <> 0. (TOP-REAL 2)
by A27, RLVECT_1:21;
then
|.(|[w1,v1]| - b).| <> 0
by EUCLID_2:42;
then reconsider q2 =
|.(|[w1,v1]| - b).| as
positive Real ;
A29:
q2 < q1
by A26, TOPREAL9:7;
A30:
q1 <= b `2
by XXREAL_0:17;
then A31:
Ball (
b,
q1)
c= y>=0-plane
by A4, Th20;
Ball (
b,
q1)
misses y=0-line
by A30, A4, Th21;
then A32:
Ball (
b,
q1)
c= y>=0-plane \ y=0-line
by A31, XBOOLE_1:86;
w1 in RAT
by RAT_1:def 2;
then
|[w1,v1]| in product <*RAT,RAT*>
by A28, FINSEQ_3:124;
then A33:
|[w1,v1]| in A
by A32, A26, A1, XBOOLE_0:def 4;
A34:
(
s = |[w1,v1]| or
s <> |[w1,v1]| )
;
consider w2,
v2 being
Rational such that A35:
|[w2,v2]| in Ball (
b,
q2)
and
|[w2,v2]| <> b
by A4, Th31;
A36:
|[w2,v2]| <> |[w1,v1]|
by A35, TOPREAL9:7;
|.(|[w2,v2]| - b).| < q2
by A35, TOPREAL9:7;
then A37:
|.(|[w2,v2]| - b).| < q1
by A29, XXREAL_0:2;
then A38:
|[w2,v2]| in Ball (
b,
q1)
by TOPREAL9:7;
A39:
q1 <= q
by XXREAL_0:17;
then
|.(|[w2,v2]| - b).| < q
by A37, XXREAL_0:2;
then
|[w2,v2]| in Ball (
b,
q)
by TOPREAL9:7;
then A40:
|[w2,v2]| in U
by A24, A38, A31, XBOOLE_0:def 4;
A41:
v2 in RAT
by RAT_1:def 2;
w2 in RAT
by RAT_1:def 2;
then
|[w2,v2]| in product <*RAT,RAT*>
by A41, FINSEQ_3:124;
then
|[w2,v2]| in A
by A32, A38, A1, XBOOLE_0:def 4;
then A42:
(
|[w1,v1]| in A \ {s} or
|[w2,v2]| in A \ {s} )
by A34, A36, A33, ZFMISC_1:56;
q2 < q
by A39, A29, XXREAL_0:2;
then
|[w1,v1]| in Ball (
b,
q)
by TOPREAL9:7;
then
|[w1,v1]| in U
by A24, A26, A31, XBOOLE_0:def 4;
hence
U meets A \ {s}
by A42, A40, XBOOLE_0:3;
verum end;
end;
hence
x in Cl (A \ {s})
by TOPGEN_2:10; verum