let n be Element of NAT ; :: thesis: for x being Point of (TOP-REAL n) holds cl_Ball (x,0) = {x}

let x be Point of (TOP-REAL n); :: thesis: cl_Ball (x,0) = {x}

thus cl_Ball (x,0) c= {x} :: according to XBOOLE_0:def 10 :: thesis: {x} c= cl_Ball (x,0)

assume a in {x} ; :: thesis: a in cl_Ball (x,0)

then A2: a = x by TARSKI:def 1;

|.(x - x).| = 0 by TOPRNS_1:28;

hence a in cl_Ball (x,0) by A2, TOPREAL9:8; :: thesis: verum

let x be Point of (TOP-REAL n); :: thesis: cl_Ball (x,0) = {x}

thus cl_Ball (x,0) c= {x} :: according to XBOOLE_0:def 10 :: thesis: {x} c= cl_Ball (x,0)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} or a in cl_Ball (x,0) )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in cl_Ball (x,0) or a in {x} )

assume A1: a in cl_Ball (x,0) ; :: thesis: a in {x}

then reconsider a = a as Point of (TOP-REAL n) ;

|.(a - x).| = 0 by A1, TOPREAL9:8;

then a = x by TOPRNS_1:28;

hence a in {x} by TARSKI:def 1; :: thesis: verum

end;assume A1: a in cl_Ball (x,0) ; :: thesis: a in {x}

then reconsider a = a as Point of (TOP-REAL n) ;

|.(a - x).| = 0 by A1, TOPREAL9:8;

then a = x by TOPRNS_1:28;

hence a in {x} by TARSKI:def 1; :: thesis: verum

assume a in {x} ; :: thesis: a in cl_Ball (x,0)

then A2: a = x by TARSKI:def 1;

|.(x - x).| = 0 by TOPRNS_1:28;

hence a in cl_Ball (x,0) by A2, TOPREAL9:8; :: thesis: verum