theorem :: TOPREAL3:28

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