south_halfline p = { |[(p `1),r]| where r is Real : r <= p `2 } by TOPREAL1:35;
hence south_halfline p is convex by Lm13; :: thesis: verum