theorem Th41: :: JORDAN1K:41

for n being Nat
for D being Subset of (TOP-REAL n)
for A, C being non empty Subset of (TOP-REAL n) st C c= D holds
dist_min (A,D) <= dist_min (A,C)