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
( p in Cl A iff for r being real number st r > 0 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
( p in Cl A iff for r being real number st r > 0 holds
Ball p',r meets A )
let p be Point of ; :: thesis: for p' being Point of st p = p' holds
( p in Cl A iff for r being real number st r > 0 holds
Ball p',r meets A )
let p' be Point of ; :: thesis: ( p = p' implies ( p in Cl A iff for r being real number st r > 0 holds
Ball p',r meets A ) )
assume A1: p = p' ; :: thesis: ( p in Cl A iff for r being real number st r > 0 holds
Ball p',r meets A )

hereby :: thesis: ( ( for r being real number st r > 0 holds
Ball p',r meets A ) implies p in Cl A )

assume A2: p in Cl A ; :: thesis: for r being real number st r > 0 holds
Ball p',r meets A
let r be real number ; :: thesis: ( r > 0 implies Ball p',r meets A )
reconsider B = Ball p',r as Subset of by TOPREAL3:13;
assume r > 0 ; :: thesis: Ball p',r meets A
then B is a_neighborhood of p by A1, GOBOARD6:5;
hence Ball p',r meets A by A2, CONNSP_2:34; :: thesis: verum

end;

assume A3: for r being real number st r > 0 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 ex r being real number st
( r > 0 & Ball p',r c= G ) by A1, GOBOARD6:8;
hence G meets A by A3, XBOOLE_1:63; :: thesis: verum

end;

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