theorem Th35: :: TOPREAL1:35

for p being Point of (TOP-REAL 2) holds south_halfline p = { |[(p `1),r]| where r is Real : r <= p `2 }