let n be Element of NAT ; :: thesis: for A being closed Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st not p in A holds
ex r being positive real number st Ball p,r misses A
let A be closed Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) st not p in A holds
ex r being positive real number st Ball p,r misses A
let p be Point of (TOP-REAL n); :: thesis: ( not p in A implies ex r being positive real number st Ball p,r misses A )
assume not p in A ; :: thesis: ex r being positive real number st Ball p,r misses A
then A1: p in A ` by SUBSET_1:50;
reconsider e = p as Point of (Euclid n) by TOPREAL3:13;
X: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider AA = A ` as Subset of (TopSpaceMetr (Euclid n)) ;
A ` is open ;
then AA is open by X, PRE_TOPC:60;
then consider r being real number such that
A2: r > 0 and
A3: Ball e,r c= A ` by A1, TOPMETR:22;
reconsider r = r as positive real number by A2;
take r ; :: thesis: Ball p,r misses A
Ball p,r = Ball e,r by TOPREAL9:13;
hence Ball p,r misses A by A3, SUBSET_1:43; :: thesis: verum