let n be Element of NAT ; :: thesis: for A being Subset of
for p being Point of
for p' being Point of st p = p' 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 p',r meets A )
let A be Subset of ; :: thesis: for p being Point of
for p' being Point of st p = p' 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 p',r meets A )
let p be Point of ; :: thesis: for p' being Point of st p = p' 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 p',r meets A )
let p' be Point of ; :: thesis: ( p = p' 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 p',r meets A ) )
assume A1: p = p' ; :: 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 p',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 p',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 p',r meets A )

hereby :: thesis: ( ( for r being real number st 0 < r & r < s holds
Ball p',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 p',r meets A
let r be real number ; :: thesis: ( 0 < r & r < s implies Ball p',r meets A )
assume that
A4: 0 < r and
r < s ; :: thesis: Ball p',r meets A
reconsider B = Ball p',r as Subset of by TOPREAL3:13;
B is a_neighborhood of p by A1, A4, Th5;
hence Ball p',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 p',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 r' being real number such that
A6: r' > 0 and
A7: Ball p',r' c= G by A1, Th8;
set r = min r',(s1 / 2);
reconsider rr = min r',(s1 / 2), rr' = r' as Real by XREAL_0:def 1;
Ball p',rr c= Ball p',rr' by PCOMPS_1:1, XXREAL_0:17;
then A8: Ball p',(min r',(s1 / 2)) c= G by A7, XBOOLE_1:1;
( s1 / 2 < s1 & min r',(s1 / 2) <= s1 / 2 ) by A2, XREAL_1:218, XXREAL_0:17;
then A9: min r',(s1 / 2) < s by XXREAL_0:2;
s1 / 2 > 0 by A2, XREAL_1:217;
then min r',(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