east_halfline p = { |[r,(p `2 )]| where r is Element of REAL : r >= p `1 } by TOPREAL1:40;
hence east_halfline p is convex by Lm12; :: thesis: verum