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