for p being Point of (TOP-REAL 2) holds north_halfline p = { |[(p `1),r]| where r is Real : r >= p `2 }