theorem Th37: :: TOPREAL1:37

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