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