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