theorem :: SPPOL_1:18

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