theorem :: TOPREAL1:3

for p, p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= p2 `1 & p in LSeg (p1,p2) holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )