theorem Th3: :: JORDAN18:3
for a being Point of (TOP-REAL 2) holds proj2 .: (north_halfline a) is bounded_below