theorem :: TOPREAL1:34

for p being Point of (TOP-REAL 2) holds south_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) }