let n be Element of 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:13;
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:218;
hence not y in Ball x9,r by METRIC_1:12; :: thesis: verum