theorem Th10: :: JORDAN1K:10

for r being Real
for M being non empty MetrSpace
for C being non empty Subset of (TopSpaceMetr M)
for p being Point of M st ( for q being Point of M st q in C holds
dist (p,q) >= r ) holds
(dist_min C) . p >= r