theorem :: JORDAN1B:8

for p, q being Point of (TOP-REAL 2) st p <> q & LSeg (p,q) is horizontal holds
<*p,q*> is being_S-Seq