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
not Segment A,p1,p2,q1,q2 is empty
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 not Segment A,p1,p2,q1,q2 is empty )
assume that
A is_an_arc_of p1,p2 and
A1: LE q1,q2,A,p1,p2 ; :: thesis: not Segment A,p1,p2,q1,q2 is empty
A2: 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;
q2 in A by A1, JORDAN5C:def 3;
then LE q2,q2,A,p1,p2 by JORDAN5C:9;
then q2 in Segment A,p1,p2,q1,q2 by A1, A2;
hence not Segment A,p1,p2,q1,q2 is empty ; :: thesis: verum