theorem Th33: :: TOPREAL1:33

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