let n be Element of NAT ; :: thesis: for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
for s being real number st s > 0 holds
( p in Cl A iff for r being real number st 0 < r & r < s holds
Ball p9,r meets A )
let A be Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
for s being real number st s > 0 holds
( p in Cl A iff for r being real number st 0 < r & r < s holds
Ball p9,r meets A )
let p be Point of (TOP-REAL n); :: thesis: for p9 being Point of (Euclid n) st p = p9 holds
for s being real number st s > 0 holds
( p in Cl A iff for r being real number st 0 < r & r < s holds
Ball p9,r meets A )
let p9 be Point of (Euclid n); :: thesis: ( p = p9 implies for s being real number st s > 0 holds
( p in Cl A iff for r being real number st 0 < r & r < s holds
Ball p9,r meets A ) )
assume A1: p = p9 ; :: thesis: for s being real number st s > 0 holds
( p in Cl A iff for r being real number st 0 < r & r < s holds
Ball p9,r meets A )
let s be real number ; :: thesis: ( s > 0 implies ( p in Cl A iff for r being real number st 0 < r & r < s holds
Ball p9,r meets A ) )
assume A2: s > 0 ; :: thesis: ( p in Cl A iff for r being real number st 0 < r & r < s holds
Ball p9,r meets A )

hereby :: thesis: ( ( for r being real number st 0 < r & r < s holds
Ball p9,r meets A ) implies p in Cl A )

assume A3: p in Cl A ; :: thesis: for r being real number st 0 < r & r < s holds
Ball p9,r meets A
let r be real number ; :: thesis: ( 0 < r & r < s implies Ball p9,r meets A )
assume that
A4: 0 < r and
r < s ; :: thesis: Ball p9,r meets A
reconsider B = Ball p9,r as Subset of (TOP-REAL n) by TOPREAL3:13;
B is a_neighborhood of p by A1, A4, Th5;
hence Ball p9,r meets A by A3, CONNSP_2:34; :: thesis: verum

end;

reconsider s1 = s as Real by XREAL_0:def 1;
assume A5: for r being real number st 0 < r & r < s holds
Ball p9,r meets A ; :: thesis: p in Cl A
for G being a_neighborhood of p holds G meets A

proof

let G be a_neighborhood of p; :: thesis: G meets A
p in Int G by CONNSP_2:def 1;
then consider r9 being real number such that
A6: r9 > 0 and
A7: Ball p9,r9 c= G by A1, Th8;
set r = min r9,(s1 / 2);
reconsider rr = min r9,(s1 / 2), rr9 = r9 as Real by XREAL_0:def 1;
Ball p9,rr c= Ball p9,rr9 by PCOMPS_1:1, XXREAL_0:17;
then A8: Ball p9,(min r9,(s1 / 2)) c= G by A7, XBOOLE_1:1;
( s1 / 2 < s1 & min r9,(s1 / 2) <= s1 / 2 ) by A2, XREAL_1:218, XXREAL_0:17;
then A9: min r9,(s1 / 2) < s by XXREAL_0:2;
s1 / 2 > 0 by A2, XREAL_1:217;
then min r9,(s1 / 2) > 0 by A6, XXREAL_0:15;
hence G meets A by A5, A8, A9, XBOOLE_1:63; :: thesis: verum

end;

hence p in Cl A by CONNSP_2:34; :: thesis: verum