theorem :: JORDAN:9

for r being Real
for p1, p2 being Point of (TOP-REAL 2) st p1 `2 <= r & r <= p2 `2 holds
LSeg (p1,p2) meets Horizontal_Line r