let X be RealUnitarySpace; :: 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 (RUSp2RNSp 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 (RUSp2RNSp X))
let r be Real; :: thesis: { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm (RUSp2RNSp X))
reconsider z = x as Element of (MetricSpaceNorm (RUSp2RNSp 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 (RUSp2RNSp X)) ) by Th2, PCOMPS_1:29;
hence { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm (RUSp2RNSp X)) by PRE_TOPC:def 2; :: thesis: verum