let A be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 holds
( q1 in Segment A,p1,p2,q1,q2 & q2 in Segment A,p1,p2,q1,q2 )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 implies ( q1 in Segment A,p1,p2,q1,q2 & q2 in Segment A,p1,p2,q1,q2 ) )
A1: L_Segment A,p1,p2,q2 = { q where q is Point of (TOP-REAL 2) : LE q,q2,A,p1,p2 } by JORDAN6:def 3;
A2: R_Segment A,p1,p2,q1 = { q where q is Point of (TOP-REAL 2) : LE q1,q,A,p1,p2 } by JORDAN6:def 4;
A3: Segment A,p1,p2,q1,q2 = (R_Segment A,p1,p2,q1) /\ (L_Segment A,p1,p2,q2) by JORDAN6:def 5;
assume that
A4: A is_an_arc_of p1,p2 and
A5: LE q1,q2,A,p1,p2 ; :: thesis: ( q1 in Segment A,p1,p2,q1,q2 & q2 in Segment A,p1,p2,q1,q2 )
A6: q1 in A by A5, JORDAN5C:def 3;
A7: q2 in A by A5, JORDAN5C:def 3;
A8: q1 in L_Segment A,p1,p2,q2 by A1, A5;
q1 in R_Segment A,p1,p2,q1 by A4, A6, Th8;
hence q1 in Segment A,p1,p2,q1,q2 by A3, A8, XBOOLE_0:def 4; :: thesis: q2 in Segment A,p1,p2,q1,q2
A9: q2 in R_Segment A,p1,p2,q1 by A2, A5;
q2 in L_Segment A,p1,p2,q2 by A4, A7, Th7;
hence q2 in Segment A,p1,p2,q1,q2 by A3, A9, XBOOLE_0:def 4; :: thesis: verum