let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) 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 (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 implies q1 = q2 )
assume A1: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 ) ; :: thesis: q1 = q2
then consider f being Function of I[01] ,((TOP-REAL 2) | P) such that
A2: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by TOPREAL1:def 2;
A3: dom f = [#] I[01] by A2, TOPS_2:def 5
.= the carrier of I[01] ;
A4: rng f = [#] ((TOP-REAL 2) | P) by A2, TOPS_2:def 5
.= P by PRE_TOPC:def 10 ;
then q2 in rng f by A1, Def3;
then consider x being set such that
A5: ( x in dom f & q2 = f . x ) by FUNCT_1:def 5;
[.0 ,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def 1;
then consider s3 being Real such that
A6: ( s3 = x & 0 <= s3 & s3 <= 1 ) by A3, A5, BORSUK_1:83;
q1 in rng f by A1, A4, Def3;
then consider y being set such that
A7: ( y in dom f & q1 = f . y ) by FUNCT_1:def 5;
[.0 ,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def 1;
then consider s4 being Real such that
A8: ( s4 = y & 0 <= s4 & s4 <= 1 ) by A3, A7, BORSUK_1:83;
A9: s3 <= s4 by A1, A2, A5, A6, A7, A8, Def3;
s4 <= s3 by A1, A2, A5, A6, A7, A8, Def3;
hence q1 = q2 by A5, A6, A7, A8, A9, XXREAL_0:1; :: thesis: verum