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)
proof
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;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} or a in 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