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