for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & r in LSeg (p,q) holds
p `2 = r `2