let A be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st 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: ( LE q1,q2,A,p1,p2 implies ( q1 in Segment (A,p1,p2,q1,q2) & q2 in Segment (A,p1,p2,q1,q2) ) )
A1: Segment (A,p1,p2,q1,q2) = (R_Segment (A,p1,p2,q1)) /\ (L_Segment (A,p1,p2,q2)) by JORDAN6:def 5;
assume A2: LE q1,q2,A,p1,p2 ; :: thesis: ( q1 in Segment (A,p1,p2,q1,q2) & q2 in Segment (A,p1,p2,q1,q2) )
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;
then A3: q1 in L_Segment (A,p1,p2,q2) by A2;
q1 in A by A2, JORDAN5C:def 3;
then q1 in R_Segment (A,p1,p2,q1) by Th4;
hence q1 in Segment (A,p1,p2,q1,q2) by A1, A3, XBOOLE_0:def 4; :: thesis: q2 in Segment (A,p1,p2,q1,q2)
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;
then A4: q2 in R_Segment (A,p1,p2,q1) by A2;
q2 in A by A2, JORDAN5C:def 3;
then q2 in L_Segment (A,p1,p2,q2) by Th3;
hence q2 in Segment (A,p1,p2,q1,q2) by A1, A4, XBOOLE_0:def 4; :: thesis: verum