let M be non empty Reflexive discerning MetrStruct ; :: thesis: for z being Point of M holds Sphere z,0 = {z}
let z be Point of M; :: thesis: Sphere z,0 = {z}
thus Sphere z,0 c= {z} :: according to XBOOLE_0:def 10 :: thesis: {z} c= Sphere z,0

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Sphere z,0 or a in {z} )
assume A1: a in Sphere z,0 ; :: thesis: a in {z}
then reconsider b = a as Point of M ;
dist z,b = 0 by A1, METRIC_1:14;
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 Sphere z,0 )
assume a in {z} ; :: thesis: a in Sphere z,0
then A2: a = z by TARSKI:def 1;
dist z,z = 0 by METRIC_1:1;
hence a in Sphere z,0 by A2, METRIC_1:14; :: thesis: verum