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:8;
B is a_neighborhood of p by A1, A4, Th5;
hence Ball (p9,r) meets A by A3, CONNSP_2:27; :: 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:216, XXREAL_0:17;
then A9: min (r9,(s1 / 2)) < s by XXREAL_0:2;
s1 / 2 > 0 by A2, XREAL_1:215;
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:27; :: thesis: verum