let n be Nat; :: thesis:
let p1, p2, q1 be Point of (TOP-REAL n); :: thesis:
assume that
A1: ( p1 <> p2 or p2 <> q1 ) and
A2: (LSeg p1,p2) /\ (LSeg p2,q1) = {p2} ; :: thesis:

per cases by A1;

suppose p1 <> p2 ; :: thesis:

hence (LSeg p1,p2) \/ (LSeg p2,q1) is_an_arc_of p1,q1 by A2, Th15, Th16; :: thesis:

end;

suppose p2 <> q1 ; :: thesis:

hence (LSeg p1,p2) \/ (LSeg p2,q1) is_an_arc_of p1,q1 by A2, Th15, Th17; :: thesis:

end;

end;