theorem Th40: :: JORDAN1K:40

for n being Nat
for r being Real
for A, B being non empty Subset of (TOP-REAL n) st ( for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ) holds
dist_min (A,B) >= r