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 = cl_Ball (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 = cl_Ball (z,r) holds
A is closed
let r be Real; :: 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:3; :: thesis: verum