let S be RealNormSpace; :: thesis: for p being Element of S
for r being Real st 0 < r holds
Ball (p,r) is Neighbourhood of p
let p be Element of S; :: thesis: for r being Real st 0 < r holds
Ball (p,r) is Neighbourhood of p
let r be Real; :: thesis: ( 0 < r implies Ball (p,r) is Neighbourhood of p )
assume 0 < r ; :: thesis: Ball (p,r) is Neighbourhood of p
then { y where y is Point of S : ||.(y - p).|| < r } is Neighbourhood of p by NFCONT_1:3;
hence Ball (p,r) is Neighbourhood of p by LMBALL; :: thesis: verum