let M be non empty MetrSpace; :: thesis: for X being Subset of (TopSpaceMetr M)
for p being Element of M holds
( p in Cl X iff for r being Real st 0 < r holds
X meets Ball (p,r) )
let X be Subset of (TopSpaceMetr M); :: thesis: for p being Element of M holds
( p in Cl X iff for r being Real st 0 < r holds
X meets Ball (p,r) )
let p be Element of M; :: thesis: ( p in Cl X iff for r being Real st 0 < r holds
X meets Ball (p,r) )
hereby :: thesis: ( ( for r being Real st 0 < r holds
X meets Ball (p,r) ) implies p in Cl X )
assume A1: p in Cl X ; :: thesis: for r being Real st 0 < r holds
X meets Ball (p,r)
let r be Real; :: thesis: ( 0 < r implies X meets Ball (p,r) )
assume A2: 0 < r ; :: thesis: X meets Ball (p,r)
reconsider G = Ball (p,r) as Subset of (TopSpaceMetr M) ;
dist (p,p) = 0 by METRIC_1:1;
then ( G is open & p in G ) by A2, METRIC_1:11, TOPMETR:14;
hence X meets Ball (p,r) by A1, PRE_TOPC:def 7; :: thesis: verum
end;
assume A3: for r being Real st 0 < r holds
X meets Ball (p,r) ; :: thesis: p in Cl X
now :: thesis: for G being Subset of (TopSpaceMetr M) st G is open & p in G holds
X meets G
let G be Subset of (TopSpaceMetr M); :: thesis: ( G is open & p in G implies X meets G )
assume ( G is open & p in G ) ; :: thesis: X meets G
then consider r being Real such that
A4: ( 0 < r & Ball (p,r) c= G ) by PCOMPS_1:def 4;
X meets Ball (p,r) by A3, A4;
hence X meets G by A4, XBOOLE_1:63; :: thesis: verum
end;
hence p in Cl X by PRE_TOPC:def 7; :: thesis: verum