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