west_halfline p = { |[r,(p `2 )]| where r is Element of REAL : r <= p `1 } by TOPREAL1:44;
hence west_halfline p is convex by Lm10; :: thesis: verum