let n be Element of NAT ; :: thesis: for r being real number
for x being Point of (TOP-REAL n)
for e being Point of (Euclid n) st x = e holds
cl_Ball e,r = cl_Ball x,r
let r be real number ; :: thesis: for x being Point of (TOP-REAL n)
for e being Point of (Euclid n) st x = e holds
cl_Ball e,r = cl_Ball x,r
let x be Point of (TOP-REAL n); :: thesis: for e being Point of (Euclid n) st x = e holds
cl_Ball e,r = cl_Ball x,r
let e be Point of (Euclid n); :: thesis: ( x = e implies cl_Ball e,r = cl_Ball x,r )
assume A1: x = e ; :: thesis: cl_Ball e,r = cl_Ball x,r

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: cl_Ball x,r c= cl_Ball e,r

let q be set ; :: thesis: ( q in cl_Ball e,r implies q in cl_Ball x,r )
assume A2: q in cl_Ball e,r ; :: thesis: q in cl_Ball x,r
then reconsider f = q as Point of (Euclid n) ;
reconsider p = f as Point of (TOP-REAL n) by TOPREAL3:13;
dist f,e <= r by A2, METRIC_1:13;
then |.(p - x).| <= r by A1, JGRAPH_1:45;
hence q in cl_Ball x,r ; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in cl_Ball x,r or q in cl_Ball e,r )
assume A3: q in cl_Ball x,r ; :: thesis: q in cl_Ball e,r
then reconsider q = q as Point of (TOP-REAL n) ;
reconsider f = q as Point of (Euclid n) by TOPREAL3:13;
|.(q - x).| <= r by A3, Th8;
then dist f,e <= r by A1, JGRAPH_1:45;
hence q in cl_Ball e,r by METRIC_1:13; :: thesis: verum