let M be non empty MetrSpace; :: thesis:
let A be Subset of (TopSpaceMetr M); :: thesis:
let p be Point of M; :: thesis:
reconsider p9 = p as Point of (TopSpaceMetr M) by TOPMETR:12;

hereby :: thesis:

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

end;

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

let G be a_neighborhood of p9; :: thesis:
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:

end;

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