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 p2,q,P,p1,p2 holds

q = p2

let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 implies q = p2 )

assume that

A1: P is_an_arc_of p1,p2 and

A2: LE p2,q,P,p1,p2 ; :: thesis: q = p2

q in P by A2;

then LE q,p2,P,p1,p2 by A1, JORDAN5C:10;

hence q = p2 by A1, A2, JORDAN5C:12; :: thesis: verum

q = p2

let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 implies q = p2 )

assume that

A1: P is_an_arc_of p1,p2 and

A2: LE p2,q,P,p1,p2 ; :: thesis: q = p2

q in P by A2;

then LE q,p2,P,p1,p2 by A1, JORDAN5C:10;

hence q = p2 by A1, A2, JORDAN5C:12; :: thesis: verum