let X be RealNormSpace; :: thesis: for x being Point of
for r being Real holds { y where y is Point of : ||.(x - y).|| < r } is open Subset of
let x be Point of ; :: thesis: for r being Real holds { y where y is Point of : ||.(x - y).|| < r } is open Subset of
let r be Real; :: thesis: { y where y is Point of : ||.(x - y).|| < r } is open Subset of
set V = { y where y is Point of : ||.(x - y).|| < r } ;
reconsider z = x as Element of ;
( ex t being Point of st
( t = x & Ball z,r = { y where y is Point of : ||.(t - y).|| < r } ) & Ball z,r in Family_open_set (MetricSpaceNorm X) ) by Th2, PCOMPS_1:33;
hence { y where y is Point of : ||.(x - y).|| < r } is open Subset of by PRE_TOPC:def 5; :: thesis: verum