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 set ; :: 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:50;
hence a in (B ` ) \/ C by XBOOLE_0:def 3; :: thesis: verum

end;

let a be set ; :: 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:50; :: thesis: verum

end;

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