north_halfline p = { |[(p `1 ),r]| where r is Element of REAL : r >= p `2 } by TOPREAL1:38;
hence north_halfline p is convex by Lm13; :: thesis: verum