theorem :: TOPREAL1:12

for n being Nat
for p1, p2, q1 being Point of (TOP-REAL n) st ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} holds
(LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1