theorem :: JORDAN1K:47

for n being Nat
for C being non empty Subset of (TOP-REAL n)
for D being Subset of (TOP-REAL n) st C c= D holds
for q being Point of (TOP-REAL n) holds dist (q,D) <= dist (q,C) by Th41;