let X be NormedLinearTopSpace; :: thesis: for x being Point of X
for r being Real
for V being Subset of X st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
let x be Point of X; :: thesis: for r being Real
for V being Subset of X st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
let r be Real; :: thesis: for V being Subset of X st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
let V be Subset of X; :: thesis: ( V = { y where y is Point of X : ||.(x - y).|| <= r } implies V is closed )
assume A1: V = { y where y is Point of X : ||.(x - y).|| <= r } ; :: thesis: V is closed
consider RNS being RealNormSpace such that
A2: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) ) by Def7;
reconsider V0 = V as Subset of (TopSpaceNorm RNS) by A2;
reconsider x1 = x as Point of RNS by A2;
reconsider V1 = V as Subset of (LinearTopSpaceNorm RNS) by A2, NORMSP_2:def 4;
for z being object holds
( z in { y where y is Point of X : ||.(x - y).|| <= r } iff z in { y where y is Point of RNS : ||.(x1 - y).|| <= r } )

proof

let z be object ; :: thesis: ( z in { y where y is Point of X : ||.(x - y).|| <= r } iff z in { y where y is Point of RNS : ||.(x1 - y).|| <= r } )

hereby :: thesis: ( z in { y where y is Point of RNS : ||.(x1 - y).|| <= r } implies z in { y where y is Point of X : ||.(x - y).|| <= r } )

assume z in { y where y is Point of X : ||.(x - y).|| <= r } ; :: thesis: z in { y where y is Point of RNS : ||.(x1 - y).|| <= r }
then consider y being Point of X such that
A3: ( y = z & ||.(x - y).|| <= r ) ;
reconsider y1 = y as Point of RNS by A2;
||.(x1 - y1).|| <= r by Th19, A2, A3;
hence z in { y where y is Point of RNS : ||.(x1 - y).|| <= r } by A3; :: thesis: verum

end;

assume z in { y where y is Point of RNS : ||.(x1 - y).|| <= r } ; :: thesis: z in { y where y is Point of X : ||.(x - y).|| <= r }
then consider y1 being Point of RNS such that
A4: ( y1 = z & ||.(x1 - y1).|| <= r ) ;
reconsider y = y1 as Point of X by A2;
||.(x - y).|| <= r by Th19, A2, A4;
hence z in { y where y is Point of X : ||.(x - y).|| <= r } by A4; :: thesis: verum

end;

then V0 is closed by NORMSP_2:24, A1, TARSKI:2;
then ([#] (TopSpaceNorm RNS)) \ V0 is open ;
then ([#] X) \ V is open by A2;
hence V is closed ; :: thesis: verum