let n be Nat; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: not for r being Real holds y in Ball (x9,r)
then A1: dist (x9,y9) <> 0 by METRIC_1:2;
take r ; :: thesis: 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; :: thesis: verum