west_halfline p = { |[r,(p `2 )]| where r is Element of REAL : r <= p `1 } by Th44;
then |[(p `1 ),(p `2 )]| in west_halfline p ;
hence not west_halfline p is empty ; :: thesis: verum