theorem :: TOPREAL3:11

for p being Point of (TOP-REAL 2)
for r, r1, s1 being Real st p in LSeg (|[r,r1]|,|[r,s1]|) holds
p `1 = r