let n be Nat; :: thesis: for P being Subset of (TOP-REAL n)
for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds
P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
let P be Subset of (TOP-REAL n); :: thesis: for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds
P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
let p1, p2, q1 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} implies P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: P /\ (LSeg (p2,q1)) = {p2} ; :: thesis: P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1

per cases ( p2 <> q1 or p2 = q1 ) ;

suppose p2 <> q1 ; :: thesis: P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1

then LSeg (p2,q1) is_an_arc_of p2,q1 by Th9;
hence P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A1, A2, Th2; :: thesis: verum

end;

suppose A3: p2 = q1 ; :: thesis: P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1

then A4: LSeg (p2,q1) = {q1} by RLTOPSP1:70;
q1 in P by A1, A3, Th1;
hence P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A1, A3, A4, ZFMISC_1:40; :: thesis: verum

end;

end;