let M be non empty MetrSpace; :: thesis: for p being Point of M
for A being Subset of (TopSpaceMetr M) holds
( p in Cl A iff for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist p,q < r ) )
let p be Point of M; :: thesis: for A being Subset of (TopSpaceMetr M) holds
( p in Cl A iff for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist p,q < r ) )
let A be Subset of (TopSpaceMetr M); :: thesis: ( p in Cl A iff for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist p,q < r ) )

hereby :: thesis: ( ( for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist p,q < r ) ) implies p in Cl A )

assume A1: p in Cl A ; :: thesis: for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist p,q < r )
let r be real number ; :: thesis: ( r > 0 implies ex q being Point of M st
( q in A & dist p,q < r ) )
assume r > 0 ; :: thesis: ex q being Point of M st
( q in A & dist p,q < r )
then Ball p,r meets A by A1, GOBOARD6:95;
then consider x being set such that
A2: x in Ball p,r and
A3: x in A by XBOOLE_0:3;
reconsider q = x as Point of M by A2;
take q = q; :: thesis: ( q in A & dist p,q < r )
thus q in A by A3; :: thesis: dist p,q < r
thus dist p,q < r by A2, METRIC_1:12; :: thesis: verum

end;

assume A4: for r being real number st r > 0 holds
ex q being Point of M st
( q in A & dist p,q < r ) ; :: thesis: p in Cl A
for r being real number st r > 0 holds
Ball p,r meets A

proof

let r be real number ; :: thesis: ( r > 0 implies Ball p,r meets A )
assume r > 0 ; :: thesis: Ball p,r meets A
then consider q being Point of M such that
A5: q in A and
A6: dist p,q < r by A4;
q in Ball p,r by A6, METRIC_1:12;
hence Ball p,r meets A by A5, XBOOLE_0:3; :: thesis: verum

end;

hence p in Cl A by GOBOARD6:95; :: thesis: verum