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, Th9, Th10; :: thesis:

end;

suppose p2 <> q1 ; :: thesis:

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

end;

end;