theorem Th8: :: JORDAN:8

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