let M be non empty MetrSpace; :: thesis: for p being Point of M
for q being Point of (TopSpaceMetr M)
for r being Real st p = q & r > 0 holds
Ball (p,r) is a_neighborhood of q
let p be Point of M; :: thesis: for q being Point of (TopSpaceMetr M)
for r being Real st p = q & r > 0 holds
Ball (p,r) is a_neighborhood of q
let q be Point of (TopSpaceMetr M); :: 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 (TopSpaceMetr M) by TOPMETR:12;
assume ( p = q & r > 0 ) ; :: thesis: Ball (p,r) is a_neighborhood of q
then q in A by Th1;
hence Ball (p,r) is a_neighborhood of q by CONNSP_2:3, TOPMETR:14; :: thesis: verum