let X be RealNormSpace; :: thesis: for x being Point of
for r being Real holds { y where y is Point of : ||.(x - y).|| <= r } is closed Subset of
let x be Point of ; :: thesis: for r being Real holds { y where y is Point of : ||.(x - y).|| <= r } is closed Subset of
let r be Real; :: thesis: { y where y is Point of : ||.(x - y).|| <= r } is closed Subset of
set V = { y where y is Point of : ||.(x - y).|| <= r } ;
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 { y where y is Point of : ||.(x - y).|| <= r } is closed Subset of by TOPREAL6:65; :: thesis: verum