let V be RealUnitarySpace; :: thesis: for M being Subset of (TopUnitSpace V)
for v being VECTOR of V
for r being Real st M = Sphere (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 = Sphere (v,r) holds
M is closed
let v be VECTOR of V; :: thesis: for r being Real st M = Sphere (v,r) holds
M is closed
let r be Real; :: thesis: ( M = Sphere (v,r) implies M is closed )
reconsider B = cl_Ball (v,r), C = Ball (v,r) as Subset of (TopUnitSpace V) ;
assume A1: M = Sphere (v,r) ; :: thesis: M is closed
A2: M ` = (B `) \/ C

proof

hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: (B `) \/ C c= M `

let a be object ; :: thesis: ( a in M ` implies a in (B `) \/ C )
assume A3: a in M ` ; :: thesis: a in (B `) \/ C
then reconsider e = a as Point of V ;
not a in M by A3, XBOOLE_0:def 5;
then dist (e,v) <> r by A1, BHSP_2:52;
then ( dist (e,v) < r or dist (e,v) > r ) by XXREAL_0:1;
then ( e in Ball (v,r) or not e in cl_Ball (v,r) ) by BHSP_2:41, BHSP_2:48;
then ( e in Ball (v,r) or e in (cl_Ball (v,r)) ` ) by SUBSET_1:29;
hence a in (B `) \/ C by XBOOLE_0:def 3; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (B `) \/ C or a in M ` )
assume A4: a in (B `) \/ C ; :: thesis: a in M `
then reconsider e = a as Point of V ;
( a in B ` or a in C ) by A4, XBOOLE_0:def 3;
then ( not e in cl_Ball (v,r) or e in C ) by XBOOLE_0:def 5;
then ( dist (e,v) > r or dist (e,v) < r ) by BHSP_2:41, BHSP_2:48;
then not a in M by A1, BHSP_2:52;
hence a in M ` by A4, SUBSET_1:29; :: thesis: verum

end;

( B is closed & C is open ) by Th50, Th53;
hence M is closed by A2; :: thesis: verum