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