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
Ball e,r = 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
Ball e,r = Ball x,r
let x be Point of (TOP-REAL n); :: thesis: for e being Point of (Euclid n) st x = e holds
Ball e,r = Ball x,r
let e be Point of (Euclid n); :: thesis: ( x = e implies Ball e,r = Ball x,r )
assume A1: x = e ; :: thesis: Ball e,r = Ball x,r

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

let q be set ; :: thesis: ( q in Ball e,r implies q in Ball x,r )
assume A2: q in Ball e,r ; :: thesis: q in 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:12;
then |.(p - x).| < r by A1, JGRAPH_1:45;
hence q in Ball x,r ; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in Ball x,r or q in Ball e,r )
assume A3: q in Ball x,r ; :: thesis: q in 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, Th7;
then dist f,e < r by A1, JGRAPH_1:45;
hence q in Ball e,r by METRIC_1:12; :: thesis: verum