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)
set V = { y where y is Point of X : ||.(x - y).|| < r } ;
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:33;
hence { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm X) by PRE_TOPC:def 5; :: thesis: verum