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