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 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 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 st r > 0 holds
ex q being Point of M st
( q in A & dist (p,q) < r ) )

hereby :: thesis: ( ( for r being Real 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 st r > 0 holds
ex q being Point of M st
( q in A & dist (p,q) < r )
let r be Real; :: 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:92;
then consider x being object 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:11; :: thesis: verum

end;

assume A4: for r being Real 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 st r > 0 holds
Ball (p,r) meets A

proof

let r be Real; :: 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:11;
hence Ball (p,r) meets A by A5, XBOOLE_0:3; :: thesis: verum

end;

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