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 = cl_Ball 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 = cl_Ball z,r holds
A is closed
let r be real number ; :: thesis: for A being Subset of (TopSpaceMetr M) st A = cl_Ball z,r holds
A is closed
let A be Subset of (TopSpaceMetr M); :: thesis: ( A = cl_Ball z,r implies A is closed )
assume A = cl_Ball z,r ; :: thesis: A is closed
then A ` is open by Lm1;
hence A is closed by TOPS_1:29; :: thesis: verum