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} & q > 0 ) by A4, A5, A6;
reconsider q = q as positive Real by A7;
consider w1, v1 being rational number such that
A8: ( |[w1,v1]| in Ball |[(b `1 ),q]|,q & |[w1,v1]| <> |[(b `1 ),q]| ) by Th35;
set q2 = |.(|[w1,v1]| - |[(b `1 ),q]|).|;
|[w1,v1]| - |[(b `1 ),q]| <> 0. (TOP-REAL 2) by A8, EUCLID:47;
then ( |.(|[w1,v1]| - |[(b `1 ),q]|).| >= 0 & |.(|[w1,v1]| - |[(b `1 ),q]|).| <> 0 ) by EUCLID_2:64;
then reconsider q2 = |.(|[w1,v1]| - |[(b `1 ),q]|).| as real positive number ;
consider w2, v2 being rational number such that
A9: ( |[w2,v2]| in Ball |[(b `1 ),q]|,q2 & |[w2,v2]| <> |[(b `1 ),q]| ) by Th35;
( |.(|[w2,v2]| - |[(b `1 ),q]|).| < q2 & q2 < q ) by A8, A9, TOPREAL9:7;
then |.(|[w2,v2]| - |[(b `1 ),q]|).| < q by XXREAL_0:2;
then A10: ( |[w2,v2]| <> |[w1,v1]| & |[w2,v2]| in Ball |[(b `1 ),q]|,q ) by A9, TOPREAL9:7;
( Ball |[(b `1 ),q]|,q c= y>=0-plane & Ball |[(b `1 ),q]|,q misses y=0-line ) by Th24, Th25;
then ( |[w1,v1]| = <*w1,v1*> & |[w2,v2]| = <*w2,v2*> & w1 in RAT & v1 in RAT & w2 in RAT & v2 in RAT & Ball |[(b `1 ),q]|,q c= y>=0-plane \ y=0-line ) by RAT_1:def 2, XBOOLE_1:86;
then ( |[w1,v1]| in y>=0-plane \ y=0-line & |[w1,v1]| in product <*RAT ,RAT *> & |[w2,v2]| in y>=0-plane \ y=0-line & |[w2,v2]| in product <*RAT ,RAT *> ) by A8, A10, FUNCT_6:2;
then A11: ( |[w1,v1]| in U & |[w2,v2]| in U & |[w1,v1]| in A & |[w2,v2]| in A ) by A1, A7, A8, A10, XBOOLE_0:def 3, XBOOLE_0:def 4;
( s = |[w1,v1]| or s <> |[w1,v1]| ) ;
then ( |[w1,v1]| in A \ {s} or |[w2,v2]| in A \ {s} ) by A10, A11, ZFMISC_1:64;
hence U meets A \ {s} by A11, XBOOLE_0:3; :: thesis: verum

end;

suppose A12: 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
A13: ( U = (Ball b,q) /\ y>=0-plane & q > 0 ) by A4, A5;
reconsider q = q, b2 = b `2 as positive Real by A12, A13;
reconsider q1 = min q,b2 as positive Real by XXREAL_0:def 9;
consider w1, v1 being rational number such that
A14: ( |[w1,v1]| in Ball b,q1 & |[w1,v1]| <> b ) by A4, Th35;
set q2 = |.(|[w1,v1]| - b).|;
|[w1,v1]| - b <> 0. (TOP-REAL 2) by A14, EUCLID:47;
then ( |.(|[w1,v1]| - b).| >= 0 & |.(|[w1,v1]| - b).| <> 0 ) by EUCLID_2:64;
then reconsider q2 = |.(|[w1,v1]| - b).| as real positive number ;
consider w2, v2 being rational number such that
A15: ( |[w2,v2]| in Ball b,q2 & |[w2,v2]| <> b ) by A4, Th35;
A16: ( |.(|[w2,v2]| - b).| < q2 & q2 < q1 ) by A14, A15, TOPREAL9:7;
then ( |.(|[w2,v2]| - b).| < q1 & q1 <= q ) by XXREAL_0:2, XXREAL_0:17;
then A17: ( |[w2,v2]| in Ball b,q1 & |.(|[w2,v2]| - b).| < q & q2 < q ) by A16, TOPREAL9:7, XXREAL_0:2;
then A18: ( |[w2,v2]| <> |[w1,v1]| & |[w1,v1]| in Ball b,q & |[w2,v2]| in Ball b,q ) by A15, TOPREAL9:7;
q1 <= b `2 by XXREAL_0:17;
then A19: ( Ball b,q1 c= y>=0-plane & Ball b,q1 misses y=0-line ) by A4, Th24, Th25;
then ( |[w1,v1]| = <*w1,v1*> & |[w2,v2]| = <*w2,v2*> & w1 in RAT & v1 in RAT & w2 in RAT & v2 in RAT & Ball b,q1 c= y>=0-plane \ y=0-line ) by RAT_1:def 2, XBOOLE_1:86;
then ( |[w1,v1]| in y>=0-plane \ y=0-line & |[w1,v1]| in product <*RAT ,RAT *> & |[w2,v2]| in y>=0-plane \ y=0-line & |[w2,v2]| in product <*RAT ,RAT *> ) by A14, A17, FUNCT_6:2;
then A20: ( |[w1,v1]| in U & |[w2,v2]| in U & |[w1,v1]| in A & |[w2,v2]| in A ) by A1, A13, A14, A17, A18, A19, XBOOLE_0:def 4;
( s = |[w1,v1]| or s <> |[w1,v1]| ) ;
then ( |[w1,v1]| in A \ {s} or |[w2,v2]| in A \ {s} ) by A18, A20, ZFMISC_1:64;
hence U meets A \ {s} by A20, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

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