let M be non empty MetrSpace; :: thesis: for X being Subset of M
for Y being Subset of (TopSpaceMetr M)
for x being Element of M
for y being Element of (TopSpaceMetr M) st X = Y & x = y holds
( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
let X be Subset of M; :: thesis: for Y being Subset of (TopSpaceMetr M)
for x being Element of M
for y being Element of (TopSpaceMetr M) st X = Y & x = y holds
( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
let Y be Subset of (TopSpaceMetr M); :: thesis: for x being Element of M
for y being Element of (TopSpaceMetr M) st X = Y & x = y holds
( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
let x be Element of M; :: thesis: for y being Element of (TopSpaceMetr M) st X = Y & x = y holds
( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )
let y be Element of (TopSpaceMetr M); :: thesis: ( X = Y & x = y implies ( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} ) )
assume A1: ( X = Y & x = y ) ; :: thesis: ( y is_an_accumulation_point_of Y iff for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} )

hereby :: thesis: ( ( for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} ) implies y is_an_accumulation_point_of Y )

assume y is_an_accumulation_point_of Y ; :: thesis: for r being Real st 0 < r holds
Ball (x,r) meets X \ {x}
then A2: y in Der Y by TOPGEN_1:16;
let r be Real; :: thesis: ( 0 < r implies Ball (x,r) meets X \ {x} )
assume A3: 0 < r ; :: thesis: Ball (x,r) meets X \ {x}
reconsider U = Ball (x,r) as Subset of (TopSpaceMetr M) ;
A4: U is open by TOPMETR:14;
dist (x,x) = 0 by METRIC_1:1;
then consider z being Point of (TopSpaceMetr M) such that
A5: ( z in Y /\ U & y <> z ) by A1, A2, A3, A4, METRIC_1:11, TOPGEN_1:17;
( z in Y & z in U & not z in {y} ) by A5, TARSKI:def 1, XBOOLE_0:def 4;
then ( z in Y \ {y} & z in U ) by XBOOLE_0:def 5;
hence Ball (x,r) meets X \ {x} by A1, XBOOLE_0:def 4; :: thesis: verum

end;

assume A6: for r being Real st 0 < r holds
Ball (x,r) meets X \ {x} ; :: thesis: y is_an_accumulation_point_of Y
for U being open Subset of (TopSpaceMetr M) st y in U holds
ex z being Point of (TopSpaceMetr M) st
( z in Y /\ U & y <> z )

proof

let U be open Subset of (TopSpaceMetr M); :: thesis: ( y in U implies ex z being Point of (TopSpaceMetr M) st
( z in Y /\ U & y <> z ) )
assume A7: y in U ; :: thesis: ex z being Point of (TopSpaceMetr M) st
( z in Y /\ U & y <> z )
U is open ;
then consider r being Real such that
A8: ( 0 < r & Ball (x,r) c= U ) by A1, A7, PCOMPS_1:def 4;
Ball (x,r) meets X \ {x} by A6, A8;
then consider z being object such that
A9: z in (Ball (x,r)) /\ (X \ {x}) by XBOOLE_0:def 1;
( z in Ball (x,r) & z in X \ {x} ) by A9, XBOOLE_0:def 4;
then A10: ( z in U & z in Y & not z in {x} ) by A1, A8, XBOOLE_0:def 5;
reconsider z = z as Point of (TopSpaceMetr M) by A9;
take z ; :: thesis: ( z in Y /\ U & y <> z )
thus ( z in Y /\ U & y <> z ) by A1, A10, TARSKI:def 1, XBOOLE_0:def 4; :: thesis: verum

end;

then y in Der Y by TOPGEN_1:17;
hence y is_an_accumulation_point_of Y by TOPGEN_1:16; :: thesis: verum