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