let x be Point of FMT_R^1; :: thesis: for y being Point of RealSpace
for r being Real st x = y & r > 0 holds
Ball (y,r) is a_neighborhood of x
let y be Point of RealSpace; :: thesis: for r being Real st x = y & r > 0 holds
Ball (y,r) is a_neighborhood of x
let r be Real; :: thesis: ( x = y & r > 0 implies Ball (y,r) is a_neighborhood of x )
assume that
A1: x = y and
A2: r > 0 ; :: thesis: Ball (y,r) is a_neighborhood of x
reconsider S = ].(x - r),(x + r).[ as Subset of FMT_R^1 by TOPMETR:17, FINTOPO7:def 15;
S is a_neighborhood of x by A2, Th58;
hence Ball (y,r) is a_neighborhood of x by A1, FRECHET:7; :: thesis: verum