let M be non empty MetrSpace; :: thesis: for z being Point of M
for r being real number
for A being Subset of (TopSpaceMetr M) st A = Sphere z,r holds
A is closed
let z be Point of M; :: thesis: for r being real number
for A being Subset of (TopSpaceMetr M) st A = Sphere z,r holds
A is closed
let r be real number ; :: thesis: for A being Subset of (TopSpaceMetr M) st A = Sphere z,r holds
A is closed
let A be Subset of (TopSpaceMetr M); :: thesis: ( A = Sphere z,r implies A is closed )
assume A1: A = Sphere z,r ; :: thesis: A is closed
reconsider B = cl_Ball z,r, C = Ball z,r as Subset of (TopSpaceMetr M) by TOPMETR:16;
A2: (cl_Ball z,r) ` = B ` by TOPMETR:16;
A3: A ` = (B ` ) \/ C

proof

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

let a be set ; :: thesis: ( a in A ` implies a in (B ` ) \/ C )
assume A4: a in A ` ; :: thesis: a in (B ` ) \/ C
then reconsider e = a as Point of M by TOPMETR:16;
not a in A by A4, XBOOLE_0:def 5;
then dist e,z <> r by A1, METRIC_1:14;
then ( dist e,z < r or dist e,z > r ) by XXREAL_0:1;
then ( e in Ball z,r or not e in cl_Ball z,r ) by METRIC_1:12, METRIC_1:13;
then ( e in Ball z,r or e in (cl_Ball z,r) ` ) by SUBSET_1:50;
hence a in (B ` ) \/ C by A2, 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 A ` )
assume A5: a in (B ` ) \/ C ; :: thesis: a in A `
then reconsider e = a as Point of M by TOPMETR:16;
( a in B ` or a in C ) by A5, XBOOLE_0:def 3;
then ( not e in cl_Ball z,r or e in C ) by XBOOLE_0:def 5;
then ( dist e,z > r or dist e,z < r ) by METRIC_1:12, METRIC_1:13;
then not a in A by A1, METRIC_1:14;
hence a in A ` by A5, SUBSET_1:50; :: thesis: verum

end;

( B ` is open & C is open ) by Lm1, TOPMETR:21;
then A ` is open by A3, TOPS_1:37;
hence A is closed by TOPS_1:29; :: thesis: verum