theorem :: JORDAN5B:13

for p, q being Point of (TOP-REAL 2) st p <> q holds
LSeg (p,q) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) }