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