for p, q being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C & q in BDD C & p `1 <> q `1 holds
North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_distinct