theorem Th46: :: JORDAN1K:46
for n being Nat
for A being non empty compact Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) ex q being Point of (TOP-REAL n) st
( q in A & dist (p,A) = dist (p,q) )