let M be non empty MetrSpace; :: thesis: for z being Point of M holds cl_Ball (z,0) = {z}
let z be Point of M; :: thesis: cl_Ball (z,0) = {z}
thus cl_Ball (z,0) c= {z} :: according to XBOOLE_0:def 10 :: thesis: {z} c= cl_Ball (z,0)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in cl_Ball (z,0) or a in {z} )
assume A1: a in cl_Ball (z,0) ; :: thesis: a in {z}
then reconsider b = a as Point of M ;
dist (b,z) <= 0 by A1, METRIC_1:12;
then dist (b,z) = 0 by METRIC_1:5;
then b = z by METRIC_1:2;
hence a in {z} by TARSKI:def 1; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {z} or a in cl_Ball (z,0) )
assume a in {z} ; :: thesis: a in cl_Ball (z,0)
then A2: a = z by TARSKI:def 1;
dist (z,z) = 0 by METRIC_1:1;
hence a in cl_Ball (z,0) by A2, METRIC_1:12; :: thesis: verum