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