let n be Nat; 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); 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); ( 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}
; P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1