theorem Th13: :: JORDAN1K:13

for r being Real
for M being non empty MetrSpace
for A, B being non empty Subset of (TopSpaceMetr M) st ( for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ) holds
min_dist_min (A,B) >= r