theorem Th3: :: JORDAN1A:3

for D being non empty Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in N-most D holds
p `2 = N-bound D