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 and
A3: f . 1 = p2 ; :: according to TOPREAL1:def 2 :: 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 ) )
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 A5: q1 in A by JORDAN5C:def 3;
A6: q2 in A by A4, JORDAN5C: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, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
A8: rng f = [#] ((TOP-REAL 2) | A) by A1, TOPS_2:def 5
.= A by PRE_TOPC:def 10 ;
then consider u being set such that
A9: u in dom f and
A10: q1 = f . u by A5, FUNCT_1:def 5;
reconsider s1 = u as Element of REAL by A7, A9;
consider u being set such that
A11: u in dom f and
A12: q2 = f . u by A6, A8, FUNCT_1:def 5;
reconsider s2 = u as Element of REAL by A7, A11;
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, A3; :: thesis: ( f . s1 = q1 & f . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )
thus ( q1 = f . s1 & q2 = f . s2 ) by A10, A12; :: thesis: ( 0 <= s1 & s1 <= s2 & s2 <= 1 )
A13: ( 0 <= s1 & s1 <= 1 ) by A7, A9, XXREAL_1:1;
thus 0 <= s1 by A7, A9, XXREAL_1:1; :: thesis: ( s1 <= s2 & s2 <= 1 )
( 0 <= s2 & s2 <= 1 ) by A7, A11, XXREAL_1:1;
hence s1 <= s2 by A1, A2, A3, A4, A10, A12, A13, JORDAN5C:def 3; :: thesis: s2 <= 1
thus s2 <= 1 by A7, A11, XXREAL_1:1; :: thesis: verum