theorem :: JORDAN1K:51

for A being non empty compact Subset of (TOP-REAL 2)
for B being open Subset of (TOP-REAL 2) st A c= B holds
for p being Point of (TOP-REAL 2) st not p in B holds
dist (p,B) < dist (p,A)