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

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