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
not Segment (A,p1,p2,q1,q2) is empty
let q1, q2, p1, p2 be Point of (TOP-REAL 2); :: thesis: ( LE q1,q2,A,p1,p2 implies not Segment (A,p1,p2,q1,q2) is empty )
A1: Segment (A,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,A,p1,p2 & LE q,q2,A,p1,p2 ) } by JORDAN6:29;
assume A2: LE q1,q2,A,p1,p2 ; :: thesis: not Segment (A,p1,p2,q1,q2) is empty
then q2 in A by JORDAN5C:def 3;
then LE q2,q2,A,p1,p2 by JORDAN5C:9;
then q2 in Segment (A,p1,p2,q1,q2) by A2, A1;
hence not Segment (A,p1,p2,q1,q2) is empty ; :: thesis: verum