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