let V be RealUnitarySpace; :: thesis: for M being Subset of (TopUnitSpace V)
for v being VECTOR of V
for r being Real st M = cl_Ball (v,r) holds
M is closed
let M be Subset of (TopUnitSpace V); :: thesis: for v being VECTOR of V
for r being Real st M = cl_Ball (v,r) holds
M is closed
let v be VECTOR of V; :: thesis: for r being Real st M = cl_Ball (v,r) holds
M is closed
let r be Real; :: thesis: ( M = cl_Ball (v,r) implies M is closed )
assume A1: M = cl_Ball (v,r) ; :: thesis: M is closed
for x being set holds
( x in M ` iff ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) )

proof

let x be set ; :: thesis: ( x in M ` iff ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) )
thus ( x in M ` implies ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) ) :: thesis: ( ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) implies x in M ` )

proof

assume A2: x in M ` ; :: thesis: ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q )
then reconsider e = x as Point of V ;
reconsider Q = Ball (e,((dist (e,v)) - r)) as Subset of (TopUnitSpace V) ;
take Q ; :: thesis: ( Q is open & Q c= M ` & x in Q )
thus Q is open by Th50; :: thesis: ( Q c= M ` & x in Q )
thus Q c= M ` :: thesis: x in Q

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Q or q in M ` )
assume A3: q in Q ; :: thesis: q in M `
then reconsider f = q as Point of V ;
dist (e,v) <= (dist (e,f)) + (dist (f,v)) by BHSP_1:35;
then A4: (dist (e,v)) - r <= ((dist (e,f)) + (dist (f,v))) - r by XREAL_1:9;
dist (e,f) < (dist (e,v)) - r by A3, BHSP_2:41;
then dist (e,f) < ((dist (e,f)) + (dist (f,v))) - r by A4, XXREAL_0:2;
then (dist (e,f)) - (dist (e,f)) < (((dist (e,f)) + (dist (f,v))) - r) - (dist (e,f)) by XREAL_1:9;
then 0 < (((dist (e,f)) - (dist (e,f))) + (dist (f,v))) - r ;
then dist (f,v) > r by XREAL_1:47;
then not q in M by A1, BHSP_2:48;
hence q in M ` by A3, SUBSET_1:29; :: thesis: verum

end;

not x in M by A2, XBOOLE_0:def 5;
then dist (v,e) > r by A1, BHSP_2:48;
then (dist (e,v)) - r > r - r by XREAL_1:9;
hence x in Q by BHSP_2:42; :: thesis: verum

end;

thus ( ex Q being Subset of (TopUnitSpace V) st
( Q is open & Q c= M ` & x in Q ) implies x in M ` ) ; :: thesis: verum

end;

then M ` is open by TOPS_1:25;
hence M is closed ; :: thesis: verum