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 p2,p1 & (LSeg q1,p2) /\ P = {p2} holds
(LSeg q1,p2) \/ P is_an_arc_of q1,p1
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 p2,p1 & (LSeg q1,p2) /\ P = {p2} holds
(LSeg q1,p2) \/ P is_an_arc_of q1,p1
let p1, p2, q1 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p2,p1 & (LSeg q1,p2) /\ P = {p2} implies (LSeg q1,p2) \/ P is_an_arc_of q1,p1 )
assume that
A1: P is_an_arc_of p2,p1 and
A2: (LSeg q1,p2) /\ P = {p2} ; :: thesis: (LSeg q1,p2) \/ P is_an_arc_of q1,p1

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

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

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

end;

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

then ( LSeg q1,p2 = {q1} & q1 in P ) by A1, Th4, RLTOPSP1:71;
hence (LSeg q1,p2) \/ P is_an_arc_of q1,p1 by A1, A3, ZFMISC_1:46; :: thesis: verum

end;

end;