for D being non empty Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st
( q `2 > N-bound D & p <> q )