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 & q1 <> q2 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 & q1 <> q2 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 ) )
assume that
A1: ( A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 ) and
A2: q1 <> q2 ; :: 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 )
consider g being Function of I[01],((TOP-REAL 2) | A), s1, s2 being Real such that
A3: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 ) and
A4: ( g . s1 = q1 & g . s2 = q2 ) and
A5: 0 <= s1 and
A6: s1 <= s2 and
A7: s2 <= 1 by A1, Th16;
take g ; :: thesis: 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 )
take s1 ; :: thesis: ex 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 )
take s2 ; :: thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )
thus ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 ) by A3, A4, A5; :: thesis: ( s1 < s2 & s2 <= 1 )
thus s1 < s2 by A2, A4, A6, XXREAL_0:1; :: thesis: s2 <= 1
thus s2 <= 1 by A7; :: thesis: verum