let A be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & q in A holds
q in R_Segment A,p1,p2,q
let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( A is_an_arc_of p1,p2 & q in A implies q in R_Segment A,p1,p2,q )
A1: R_Segment A,p1,p2,q = { q1 where q1 is Point of (TOP-REAL 2) : LE q,q1,A,p1,p2 } by JORDAN6:def 4;
assume ( A is_an_arc_of p1,p2 & q in A ) ; :: thesis: q in R_Segment A,p1,p2,q
then LE q,q,A,p1,p2 by JORDAN5C:9;
hence q in R_Segment A,p1,p2,q by A1; :: thesis: verum