let M be non empty MetrSpace; :: thesis: for X being Subset of M
for x being Element of M st ( for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} ) holds
for r being Real st 0 < r holds
(Ball (x,r)) /\ (X \ {x}) is infinite
let X be Subset of M; :: thesis: for x being Element of M st ( for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} ) holds
for r being Real st 0 < r holds
(Ball (x,r)) /\ (X \ {x}) is infinite
let x be Element of M; :: thesis: ( ( for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} ) implies for r being Real st 0 < r holds
(Ball (x,r)) /\ (X \ {x}) is infinite )
assume A1: for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} ; :: thesis: for r being Real st 0 < r holds
(Ball (x,r)) /\ (X \ {x}) is infinite
assume ex r being Real st
( 0 < r & not (Ball (x,r)) /\ (X \ {x}) is infinite ) ; :: thesis: contradiction
then consider r being Real such that
A2: ( 0 < r & (Ball (x,r)) /\ (X \ {x}) is finite ) ;
A3: (Ball (x,r)) /\ (X \ {x}) is finite by A2;
A4: Ball (x,r) meets X \ {x} by A1, A2;
deffunc H1( Point of M) -> object = dist (x,$1);
set D = { H1(y) where y is Element of the carrier of M : y in (Ball (x,r)) /\ (X \ {x}) } ;
A5: { H1(y) where y is Element of the carrier of M : y in (Ball (x,r)) /\ (X \ {x}) } is finite from FRAENKEL:sch 21(A3);
 A7: { H1(y) where y is Element of the carrier of M : y in (Ball (x,r)) /\ (X \ {x}) } c= REAL
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { H1(y) where y is Element of the carrier of M : y in (Ball (x,r)) /\ (X \ {x}) } or z in REAL )
assume z in { H1(y) where y is Element of the carrier of M : y in (Ball (x,r)) /\ (X \ {x}) } ; :: thesis: z in REAL
then consider y being Point of M such that
A6: ( z = dist (x,y) & y in (Ball (x,r)) /\ (X \ {x}) ) ;
thus z in REAL by A6, XREAL_0:def 1; :: thesis: verum
end;
consider w being object such that
A8: w in (Ball (x,r)) /\ (X \ {x}) by A4, XBOOLE_0:def 1;
reconsider w = w as Point of M by A8;
dist (x,w) in { H1(y) where y is Element of the carrier of M : y in (Ball (x,r)) /\ (X \ {x}) } by A8;
then reconsider D = { H1(y) where y is Element of the carrier of M : y in (Ball (x,r)) /\ (X \ {x}) } as non empty real-membered set by A7;
reconsider D = D as real-membered left_end set by A5;
set r0 = min D;
A9: ( min D in D & ( for s being Real st s in D holds
min D <= s ) ) by XXREAL_2:def 7;
consider y being Point of M such that
A10: ( min D = dist (x,y) & y in (Ball (x,r)) /\ (X \ {x}) ) by A9;
A11: y in Ball (x,r) by A10, XBOOLE_0:def 4;
y in X \ {x} by A10, XBOOLE_0:def 4;
then not y in {x} by XBOOLE_0:def 5;
then A12: y <> x by TARSKI:def 1;
then 0 < min D by A10, METRIC_1:7;
then Ball (x,((min D) / 2)) meets X \ {x} by A1;
then consider z being object such that
A13: z in (Ball (x,((min D) / 2))) /\ (X \ {x}) by XBOOLE_0:def 1;
A14: ( z in Ball (x,((min D) / 2)) & z in X \ {x} ) by A13, XBOOLE_0:def 4;
reconsider z = z as Point of M by A13;
(min D) / 2 < min D by A10, A12, METRIC_1:7, XREAL_1:216;
then A15: dist (x,z) < min D by A14, METRIC_1:11, XXREAL_0:2;
then dist (x,z) < r by A10, A11, METRIC_1:11, XXREAL_0:2;
then z in Ball (x,r) by METRIC_1:11;
then z in (Ball (x,r)) /\ (X \ {x}) by A14, XBOOLE_0:def 4;
then dist (x,z) in D ;
hence contradiction by A15, XXREAL_2:def 7; :: thesis: verum