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 set ; :: 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 Element of REAL holds BB . |[x,0 ]| = { ((Ball |[x,q]|,q) \/ {|[x,0 ]|}) where q is Element of REAL : q > 0 } and
A3: for x, y being Element of REAL st y > 0 holds
BB . |[x,y]| = { ((Ball |[x,y]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 } by Def3;
A4: a = |[(b `1 ),(b `2 )]| by EUCLID:57;
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, Th22;

suppose A6: b `2 = 0 ; :: thesis: U meets A \ {s}

then BB . a = { ((Ball |[(b `1 ),q]|,q) \/ {|[(b `1 ),0 ]|}) where q is Element of 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 number such that
A9: |[w1,v1]| in Ball |[(b `1 ),q]|,q and
A10: |[w1,v1]| <> |[(b `1 ),q]| by Th35;
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, EUCLID:47;
then |.(|[w1,v1]| - |[(b `1 ),q]|).| <> 0 by EUCLID_2:64;
then reconsider q2 = |.(|[w1,v1]| - |[(b `1 ),q]|).| as real positive number ;
A12: q2 < q by A9, TOPREAL9:7;
consider w2, v2 being rational number such that
A13: |[w2,v2]| in Ball |[(b `1 ),q]|,q2 and
|[w2,v2]| <> |[(b `1 ),q]| by Th35;
|.(|[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 Th25;
Ball |[(b `1 ),q]|,q c= y>=0-plane by Th24;
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, FUNCT_6:2;
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, FUNCT_6:2;
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:64;
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 Element of 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 number such that
A26: |[w1,v1]| in Ball b,q1 and
A27: |[w1,v1]| <> b by A4, Th35;
A28: v1 in RAT by RAT_1:def 2;
set q2 = |.(|[w1,v1]| - b).|;
|[w1,v1]| - b <> 0. (TOP-REAL 2) by A27, EUCLID:47;
then |.(|[w1,v1]| - b).| <> 0 by EUCLID_2:64;
then reconsider q2 = |.(|[w1,v1]| - b).| as real positive number ;
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, Th24;
Ball b,q1 misses y=0-line by A30, A4, Th25;
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, FUNCT_6:2;
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 number such that
A35: |[w2,v2]| in Ball b,q2 and
|[w2,v2]| <> b by A4, Th35;
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, FUNCT_6:2;
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:64;
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:11; :: thesis: verum