let X be RealNormSpace; :: thesis: for V being Subset of (LinearTopSpaceNorm X) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
let V be Subset of (LinearTopSpaceNorm X); :: thesis: ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
reconsider V0 = V as Subset of (TopSpaceNorm X) by Def4;
( V is open iff V0 is open ) by Th20;
hence ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ) by Th7; :: thesis: verum