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 number 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 number 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 number st r > 0 holds
Ball p,r meets A )
reconsider p9 = p as Point of (TopSpaceMetr M) by TOPMETR:16;

hereby :: thesis: ( ( for r being real number 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 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 (TopSpaceMetr M) by TOPMETR:16;
assume r > 0 ; :: thesis: Ball p,r meets A
then B is a_neighborhood of p9 by Th94;
hence Ball p,r meets A by A1, CONNSP_2:34; :: thesis: verum

end;

assume A2: 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 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 number st
( r > 0 & Ball p,r c= G ) by Th7;
hence G meets A by A2, XBOOLE_1:63; :: thesis: verum

end;

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