theorem Th8: :: JORDAN18:8

for a being Point of (TOP-REAL 2) holds upper_bound (proj2 .: (south_halfline a)) = a `2