let n be Nat; for x, y being Point of (TOP-REAL n)
for x9 being Point of (Euclid n) st x9 = x & x <> y holds
ex r being Real st not y in Ball (x9,r)
let x, y be Point of (TOP-REAL n); for x9 being Point of (Euclid n) st x9 = x & x <> y holds
ex r being Real st not y in Ball (x9,r)
let x9 be Point of (Euclid n); ( x9 = x & x <> y implies ex r being Real st not y in Ball (x9,r) )
reconsider y9 = y as Point of (Euclid n) by TOPREAL3:8;
reconsider r = (dist (x9,y9)) / 2 as Real ;
assume
( x9 = x & x <> y )
; not for r being Real holds y in Ball (x9,r)
then A1:
dist (x9,y9) <> 0
by METRIC_1:2;
take
r
; not y in Ball (x9,r)
dist (x9,y9) >= 0
by METRIC_1:5;
then
dist (x9,y9) > r
by A1, XREAL_1:216;
hence
not y in Ball (x9,r)
by METRIC_1:11; verum