theorem :: TOPREAL6:29

for p, q, s being Point of (TOP-REAL 2) st s in LSeg (p,q) & s <> p & s <> q & p `1 < q `1 holds
( p `1 < s `1 & s `1 < q `1 )