for p, q being Point of (TOP-REAL 2)
for r being Real st p `2 = q `2 & r in [.(proj1 . p),(proj1 . q).] holds
|[r,(p `2)]| in LSeg (p,q)