north_halfline p = { |[(p `1),r]| where r is Real : r >= p `2 } by TOPREAL1:31;
hence north_halfline p is convex by Lm15; :: thesis: verum