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