let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds
q = p1
let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 implies q = p1 )
assume A1: ( P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 ) ; :: thesis: q = p1
then q in P by JORDAN5C:def 3;
then LE p1,q,P,p1,p2 by A1, JORDAN5C:10;
hence q = p1 by A1, JORDAN5C:12; :: thesis: verum