let M be non empty MetrSpace; 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; 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); ( 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 ( ( 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
;
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;
( r > 0 implies ex q being Point of M st
( q in A & dist (p,q) < r ) )assume
r > 0
;
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;
( q in A & dist (p,q) < r )thus
q in A
by A3;
dist (p,q) < rthus
dist (
p,
q)
< r
by A2, METRIC_1:11;
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 )
; p in Cl A
for r being Real st r > 0 holds
Ball (p,r) meets A
hence
p in Cl A
by GOBOARD6:92; verum