let P be Subset of (); :: thesis: for p1, p2, q1, q2 being Point of () st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds
q1 = q2

let p1, p2, q1, q2 be Point of (); :: thesis: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 implies q1 = q2 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE q1,q2,P,p1,p2 and
A3: LE q2,q1,P,p1,p2 ; :: thesis: q1 = q2
consider f being Function of I,(() | P) such that
A4: f is being_homeomorphism and
A5: ( f . 0 = p1 & f . 1 = p2 ) by ;
A6: dom f = [#] I by
.= the carrier of I ;
A7: rng f = [#] (() | P) by
.= P by PRE_TOPC:def 5 ;
then q2 in rng f by A2;
then consider x being object such that
A8: x in dom f and
A9: q2 = f . x by FUNCT_1:def 3;
q1 in rng f by A2, A7;
then consider y being object such that
A10: y in dom f and
A11: q1 = f . y by FUNCT_1:def 3;
[.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def 1;
then consider s3 being Real such that
A12: s3 = x and
A13: ( 0 <= s3 & s3 <= 1 ) by ;
[.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def 1;
then consider s4 being Real such that
A14: s4 = y and
A15: ( 0 <= s4 & s4 <= 1 ) by ;
( s3 <= s4 & s4 <= s3 ) by A2, A3, A4, A5, A9, A12, A13, A11, A14, A15;
hence q1 = q2 by ; :: thesis: verum