for p, q being Point of (TOP-REAL 2) st p `1 = q `1 & p `2 <> q `2 holds
|[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (p,q)