let A be Subset of Niemytzki-plane; :: thesis: ( 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*>) ; :: thesis: for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane
let s be set ; :: thesis: Cl (A \ {s}) = [#] Niemytzki-plane
thus Cl (A \ {s}) c= [#] Niemytzki-plane ; :: according to XBOOLE_0:def 10 :: thesis: [#] Niemytzki-plane c= Cl (A \ {s})
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] Niemytzki-plane or x in Cl (A \ {s}) )
assume x in [#] Niemytzki-plane ; :: thesis: 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 ; :: thesis: ( U in BB . a implies U meets A \ {s} )
assume A5: U in BB . a ; :: thesis: U meets A \ {s}

per cases ( b `2 = 0 or b `2 > 0 ) by A4, Th18;

suppose A6: b `2 = 0 ; :: thesis: 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; :: thesis: verum

end;

suppose A23: b `2 > 0 ; :: thesis: 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; :: thesis: verum

end;

end;

end;

hence x in Cl (A \ {s}) by TOPGEN_2:10; :: thesis: verum