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