let M be non empty MetrSpace; :: thesis: for A being Subset of (TopSpaceMetr M)
for p being Point of M holds
( p in Cl A iff for r being Real st r > 0 holds
Ball (p,r) meets A )
let A be Subset of (TopSpaceMetr M); :: thesis: for p being Point of M holds
( p in Cl A iff for r being Real st r > 0 holds
Ball (p,r) meets A )
let p be Point of M; :: thesis: ( p in Cl A iff for r being Real st r > 0 holds
Ball (p,r) meets A )
reconsider p9 = p as Point of (TopSpaceMetr M) by TOPMETR:12;

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

assume A1: p in Cl A ; :: thesis: for r being Real st r > 0 holds
Ball (p,r) meets A
let r be Real; :: thesis: ( r > 0 implies Ball (p,r) meets A )
reconsider B = Ball (p,r) as Subset of (TopSpaceMetr M) by TOPMETR:12;
assume r > 0 ; :: thesis: Ball (p,r) meets A
then B is a_neighborhood of p9 by Th91;
hence Ball (p,r) meets A by A1, CONNSP_2:27; :: thesis: verum

end;

assume A2: for r being Real st r > 0 holds
Ball (p,r) meets A ; :: thesis: p in Cl A
for G being a_neighborhood of p9 holds G meets A

proof

let G be a_neighborhood of p9; :: thesis: G meets A
p in Int G by CONNSP_2:def 1;
then ex r being Real st
( r > 0 & Ball (p,r) c= G ) by Th4;
hence G meets A by A2, XBOOLE_1:63; :: thesis: verum

end;

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