let n be Element of NAT ; :: thesis: for x, y being Point of (TOP-REAL n)
for x' being Point of (Euclid n) st x' = x & x <> y holds
ex r being Real st not y in Ball x',r
let x, y be Point of (TOP-REAL n); :: thesis: for x' being Point of (Euclid n) st x' = x & x <> y holds
ex r being Real st not y in Ball x',r
let x' be Point of (Euclid n); :: thesis: ( x' = x & x <> y implies ex r being Real st not y in Ball x',r )
assume that
A1: x' = x and
A2: x <> y ; :: thesis: not for r being Real holds y in Ball x',r
reconsider y' = y as Point of (Euclid n) by TOPREAL3:13;
reconsider r = (dist x',y') / 2 as Real ;
take r ; :: thesis: not y in Ball x',r
A3: dist x',y' <> 0 by A1, A2, METRIC_1:2;
dist x',y' >= 0 by METRIC_1:5;
then dist x',y' > r by A3, XREAL_1:218;
hence not y in Ball x',r by METRIC_1:12; :: thesis: verum