let n be Nat; :: thesis: for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Cl A iff for r being Real st r > 0 holds
Ball (p9,r) meets A )
let A be Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
( p in Cl A iff for r being Real st r > 0 holds
Ball (p9,r) meets A )
let p be Point of (TOP-REAL n); :: thesis: for p9 being Point of (Euclid n) st p = p9 holds
( p in Cl A iff for r being Real st r > 0 holds
Ball (p9,r) meets A )
let p9 be Point of (Euclid n); :: thesis: ( p = p9 implies ( p in Cl A iff for r being Real st r > 0 holds
Ball (p9,r) meets A ) )
assume A1: p = p9 ; :: thesis: ( p in Cl A iff for r being Real st r > 0 holds
Ball (p9,r) meets A )
hereby :: thesis: ( ( for r being Real st r > 0 holds
Ball (p9,r) meets A ) implies p in Cl A )
assume A2: p in Cl A ; :: thesis: for r being Real st r > 0 holds
Ball (p9,r) meets A
let r be Real; :: thesis: ( r > 0 implies Ball (p9,r) meets A )
reconsider B = Ball (p9,r) as Subset of (TOP-REAL n) by TOPREAL3:8;
assume r > 0 ; :: thesis: Ball (p9,r) meets A
then B is a_neighborhood of p by A1, GOBOARD6:2;
hence Ball (p9,r) meets A by A2, CONNSP_2:27; :: thesis: verum
end;
assume A3: for r being Real st r > 0 holds
Ball (p9,r) meets A ; :: thesis: p in Cl A
for G being a_neighborhood of p holds G meets A
proof
let G be a_neighborhood of p; :: thesis: G meets A
p in Int G by CONNSP_2:def 1;
then ex r being Real st
( r > 0 & Ball (p9,r) c= G ) by A1, GOBOARD6:5;
hence G meets A by A3, XBOOLE_1:63; :: thesis: verum
end;
hence p in Cl A by CONNSP_2:27; :: thesis: verum