let n be Nat; :: thesis: for p being Point of (Euclid n)
for q being Point of (TOP-REAL n)
for r being Real st p = q & r > 0 holds
Ball (p,r) is a_neighborhood of q
let p be Point of (Euclid n); :: thesis: for q being Point of (TOP-REAL n)
for r being Real st p = q & r > 0 holds
Ball (p,r) is a_neighborhood of q
let q be Point of (TOP-REAL n); :: thesis: for r being Real st p = q & r > 0 holds
Ball (p,r) is a_neighborhood of q
let r be Real; :: thesis: ( p = q & r > 0 implies Ball (p,r) is a_neighborhood of q )
reconsider A = Ball (p,r) as Subset of (TOP-REAL n) by TOPREAL3:8;
A1: 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)) ;
AA is open by TOPMETR:14;
then A2: A is open by A1, PRE_TOPC:30;
assume ( p = q & r > 0 ) ; :: thesis: Ball (p,r) is a_neighborhood of q
hence Ball (p,r) is a_neighborhood of q by A2, Th1, CONNSP_2:3; :: thesis: verum