theorem Th12: :: JORDAN1K:12

for M being non empty MetrSpace
for A, B being compact Subset of (TopSpaceMetr M) st A meets B holds
min_dist_min (A,B) = 0