let X be RealNormSpace; :: thesis: for x being Point of X

for r being Real

for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds

V is open

let x be Point of X; :: thesis: for r being Real

for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds

V is open

let r be Real; :: thesis: for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds

V is open

let V be Subset of (LinearTopSpaceNorm X); :: thesis: ( V = { y where y is Point of X : ||.(x - y).|| < r } implies V is open )

reconsider V0 = V as Subset of (TopSpaceNorm X) by Def4;

assume V = { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: V is open

then V0 is open by Th8;

hence V is open by Th20; :: thesis: verum

for r being Real

for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds

V is open

let x be Point of X; :: thesis: for r being Real

for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds

V is open

let r be Real; :: thesis: for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds

V is open

let V be Subset of (LinearTopSpaceNorm X); :: thesis: ( V = { y where y is Point of X : ||.(x - y).|| < r } implies V is open )

reconsider V0 = V as Subset of (TopSpaceNorm X) by Def4;

assume V = { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: V is open

then V0 is open by Th8;

hence V is open by Th20; :: thesis: verum