theorem :: JORDAN18:10

for a being Point of (TOP-REAL 2) holds lower_bound (proj1 .: (east_halfline a)) = a `1