let A be Subset of (TOP-REAL 2); :: thesis: for q1, q2, p1, p2 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 q1, q2, p1, p2 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 Th8;
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 Th7;
hence q2 in Segment A,p1,p2,q1,q2 by A1, A4, XBOOLE_0:def 4; :: thesis: verum