theorem :: TOPREAL3:27

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