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 and
A2: LE q1,q2,A,p1,p2 and
A3: 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
A4: g is being_homeomorphism and
A5: ( g . 0 = p1 & g . 1 = p2 ) and
A6: g . s1 = q1 and
A7: g . s2 = q2 and
A8: 0 <= s1 and
A9: s1 <= s2 and
A10: s2 <= 1 by A1, A2, Th20;
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 A4, A5, A6, A7, A8; :: thesis: ( s1 < s2 & s2 <= 1 )
thus s1 < s2 by A3, A6, A7, A9, XXREAL_0:1; :: thesis: s2 <= 1
thus s2 <= 1 by A10; :: thesis: verum