theorem Th36: :: JGRAPH_1:37

for M being non empty MetrSpace
for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
min_dist_min (P,Q) >= 0