theorem Th7: :: TOPMETR4:8

for M being non empty MetrSpace
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} )