let X be RealNormSpace; :: thesis: for x being Point of
for r being Real
for V being Subset of st V = { y where y is Point of : ||.(x - y).|| <= r } holds
V is closed
let x be Point of ; :: thesis: for r being Real
for V being Subset of st V = { y where y is Point of : ||.(x - y).|| <= r } holds
V is closed
let r be Real; :: thesis: for V being Subset of st V = { y where y is Point of : ||.(x - y).|| <= r } holds
V is closed
let V be Subset of ; :: thesis: ( V = { y where y is Point of : ||.(x - y).|| <= r } implies V is closed )
assume A1: V = { y where y is Point of : ||.(x - y).|| <= r } ; :: thesis: V is closed
reconsider z = x as Element of ;
ex t being Point of st
( t = x & cl_Ball z,r = { y where y is Point of : ||.(t - y).|| <= r } ) by Th3;
hence V is closed by A1, TOPREAL6:65; :: thesis: verum