let M be non empty MetrSpace; :: thesis: for z being Point of M
for r being Real
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
for A being Subset of (TopSpaceMetr M) st A = Sphere (z,r) holds
A is closed
let r be Real; :: 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:12;
A2: (cl_Ball (z,r)) ` = B ` by TOPMETR:12;
A3: A ` = (B `) \/ C

proof

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

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

end;

A6: C is open by TOPMETR:14;
B ` is open by Lm1;
hence A is closed by A3, A6, TOPS_1:3; :: thesis: verum