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