theorem Th7: :: JORDAN18:7

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