let n be Nat; for r being Real
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; 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); 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); ( x = e implies cl_Ball (e,r) = cl_Ball (x,r) )
assume A1:
x = e
; cl_Ball (e,r) = cl_Ball (x,r)
let q be object ; TARSKI:def 3 ( not q in cl_Ball (x,r) or q in cl_Ball (e,r) )
assume A3:
q in cl_Ball (x,r)
; 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:8;
|.(q - x).| <= r
by A3, Th6;
then
dist (f,e) <= r
by A1, JGRAPH_1:28;
hence
q in cl_Ball (e,r)
by METRIC_1:12; verum