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 set ; :: 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:42;
then A4: (dist e,v) - r <= ((dist e,f) + (dist f,v)) - r by XREAL_1:11;
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:11;
then 0 < (((dist e,f) - (dist e,f)) + (dist f,v)) - r ;
then dist f,v > r by XREAL_1:49;
then not q in M by A1, BHSP_2:48;
hence q in M ` by A3, SUBSET_1:50; :: 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:11;
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:57;
hence M is closed by TOPS_1:29; :: thesis: verum