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 set ; :: 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:13;
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 set ; :: 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:13; :: thesis: verum