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
ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
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 ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 ) )
given f being Function of I[01],((TOP-REAL 2) | A) such that A1: f is being_homeomorphism and
A2: ( f . 0 = p1 & f . 1 = p2 ) ; :: according to TOPREAL1:def 1 :: thesis: ( not LE q1,q2,A,p1,p2 or ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 ) )
A3: rng f = [#] ((TOP-REAL 2) | A) by A1
.= A by PRE_TOPC:def 5 ;
assume A4: LE q1,q2,A,p1,p2 ; :: thesis: ex g being Function of I[01],((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
then q1 in A by JORDAN5C:def 3;
then consider u being object such that
A5: u in dom f and
A6: q1 = f . u by A3, FUNCT_1:def 3;
take f ; :: thesis: ex s1, s2 being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s1 = q1 & f . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
A7: dom f = [#] I[01] by A1
.= [.0,1.] by BORSUK_1:40 ;
then reconsider s1 = u as Element of REAL by A5;
A8: s1 <= 1 by A7, A5, XXREAL_1:1;
q2 in A by A4, JORDAN5C:def 3;
then consider u being object such that
A9: u in dom f and
A10: q2 = f . u by A3, FUNCT_1:def 3;
reconsider s2 = u as Element of REAL by A7, A9;
take s1 ; :: thesis: ex s2 being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s1 = q1 & f . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
take s2 ; :: thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s1 = q1 & f . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
thus ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, A2; :: thesis: ( f . s1 = q1 & f . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
thus ( q1 = f . s1 & q2 = f . s2 ) by A6, A10; :: thesis: ( 0 <= s1 & s1 <= s2 & s2 <= 1 )
thus 0 <= s1 by A7, A5, XXREAL_1:1; :: thesis: ( s1 <= s2 & s2 <= 1 )
( 0 <= s2 & s2 <= 1 ) by A7, A9, XXREAL_1:1;
hence s1 <= s2 by A1, A2, A4, A6, A10, A8, JORDAN5C:def 3; :: thesis: s2 <= 1
thus s2 <= 1 by A7, A9, XXREAL_1:1; :: thesis: verum