let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2)

for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds

LE q1,q2,P,p1,p2

let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds

LE q1,q2,P,p1,p2

let g be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds

LE q1,q2,P,p1,p2

let s1, s2 be Real; :: thesis: ( P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 implies LE q1,q2,P,p1,p2 )

assume that

A1: P is_an_arc_of p1,p2 and

A2: g is being_homeomorphism and

A3: g . 0 = p1 and

A4: g . 1 = p2 and

A5: g . s1 = q1 and

A6: ( 0 <= s1 & s1 <= 1 ) and

A7: g . s2 = q2 and

A8: ( 0 <= s2 & s2 <= 1 ) and

A9: s1 <= s2 ; :: thesis: LE q1,q2,P,p1,p2

reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;

s1 in the carrier of I[01] by A6, BORSUK_1:43;

then A10: q1 in [#] ((TOP-REAL 2) | P9) by A5, FUNCT_2:5;

reconsider g = g as Function of I[01],((TOP-REAL 2) | P9) ;

s2 in the carrier of I[01] by A8, BORSUK_1:43;

then g . s2 in the carrier of ((TOP-REAL 2) | P9) by FUNCT_2:5;

then A11: q2 in P by A7, A10, PRE_TOPC:def 5;

hence LE q1,q2,P,p1,p2 by A11, A12; :: thesis: verum

for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds

LE q1,q2,P,p1,p2

let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds

LE q1,q2,P,p1,p2

let g be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds

LE q1,q2,P,p1,p2

let s1, s2 be Real; :: thesis: ( P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 implies LE q1,q2,P,p1,p2 )

assume that

A1: P is_an_arc_of p1,p2 and

A2: g is being_homeomorphism and

A3: g . 0 = p1 and

A4: g . 1 = p2 and

A5: g . s1 = q1 and

A6: ( 0 <= s1 & s1 <= 1 ) and

A7: g . s2 = q2 and

A8: ( 0 <= s2 & s2 <= 1 ) and

A9: s1 <= s2 ; :: thesis: LE q1,q2,P,p1,p2

reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;

s1 in the carrier of I[01] by A6, BORSUK_1:43;

then A10: q1 in [#] ((TOP-REAL 2) | P9) by A5, FUNCT_2:5;

reconsider g = g as Function of I[01],((TOP-REAL 2) | P9) ;

s2 in the carrier of I[01] by A8, BORSUK_1:43;

then g . s2 in the carrier of ((TOP-REAL 2) | P9) by FUNCT_2:5;

then A11: q2 in P by A7, A10, PRE_TOPC:def 5;

A12: now :: thesis: for h being Function of I[01],((TOP-REAL 2) | P9)

for t1, t2 being Real st h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 holds

t1 <= t2

q1 in P
by A10, PRE_TOPC:def 5;for t1, t2 being Real st h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 holds

t1 <= t2

reconsider s19 = s1, s29 = s2 as Point of I[01] by A6, A8, BORSUK_1:43;

let h be Function of I[01],((TOP-REAL 2) | P9); :: thesis: for t1, t2 being Real st h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 holds

b_{4} <= b_{5}

let t1, t2 be Real; :: thesis: ( h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 implies b_{2} <= b_{3} )

assume that

A13: h is being_homeomorphism and

A14: h . 0 = p1 and

A15: h . 1 = p2 and

A16: h . t1 = q1 and

A17: ( 0 <= t1 & t1 <= 1 ) and

A18: h . t2 = q2 and

A19: ( 0 <= t2 & t2 <= 1 ) ; :: thesis: b_{2} <= b_{3}

A20: h is one-to-one by A13, TOPS_2:def 5;

set hg = (h ") * g;

h " is being_homeomorphism by A13, TOPS_2:56;

then (h ") * g is being_homeomorphism by A2, TOPS_2:57;

then A21: ( (h ") * g is continuous & (h ") * g is one-to-one ) by TOPS_2:def 5;

reconsider hg1 = ((h ") * g) . s19, hg2 = ((h ") * g) . s29 as Real by BORSUK_1:40;

A22: dom g = [#] I[01] by A2, TOPS_2:def 5;

then A23: 0 in dom g by BORSUK_1:43;

A24: dom h = [#] I[01] by A13, TOPS_2:def 5;

then A25: t1 in dom h by A17, BORSUK_1:43;

A26: 0 in dom h by A24, BORSUK_1:43;

rng h = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5;

then h is onto by FUNCT_2:def 3;

then A27: h " = h " by A20, TOPS_2:def 4;

then (h ") . p1 = 0 by A14, A26, A20, FUNCT_1:32;

then A28: ((h ") * g) . 0 = 0 by A3, A23, FUNCT_1:13;

s1 in dom g by A6, A22, BORSUK_1:43;

then A29: ((h ") * g) . s1 = (h ") . q1 by A5, FUNCT_1:13

.= t1 by A16, A20, A25, A27, FUNCT_1:32 ;

A30: t2 in dom h by A19, A24, BORSUK_1:43;

s2 in dom g by A8, A22, BORSUK_1:43;

then A31: ((h ") * g) . s2 = (h ") . q2 by A7, FUNCT_1:13

.= t2 by A18, A20, A30, A27, FUNCT_1:32 ;

A32: 1 in dom g by A22, BORSUK_1:43;

A33: 1 in dom h by A24, BORSUK_1:43;

(h ") . p2 = 1 by A15, A33, A20, A27, FUNCT_1:32;

then A34: ((h ") * g) . 1 = 1 by A4, A32, FUNCT_1:13;

end;let h be Function of I[01],((TOP-REAL 2) | P9); :: thesis: for t1, t2 being Real st h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 holds

b

let t1, t2 be Real; :: thesis: ( h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 implies b

assume that

A13: h is being_homeomorphism and

A14: h . 0 = p1 and

A15: h . 1 = p2 and

A16: h . t1 = q1 and

A17: ( 0 <= t1 & t1 <= 1 ) and

A18: h . t2 = q2 and

A19: ( 0 <= t2 & t2 <= 1 ) ; :: thesis: b

A20: h is one-to-one by A13, TOPS_2:def 5;

set hg = (h ") * g;

h " is being_homeomorphism by A13, TOPS_2:56;

then (h ") * g is being_homeomorphism by A2, TOPS_2:57;

then A21: ( (h ") * g is continuous & (h ") * g is one-to-one ) by TOPS_2:def 5;

reconsider hg1 = ((h ") * g) . s19, hg2 = ((h ") * g) . s29 as Real by BORSUK_1:40;

A22: dom g = [#] I[01] by A2, TOPS_2:def 5;

then A23: 0 in dom g by BORSUK_1:43;

A24: dom h = [#] I[01] by A13, TOPS_2:def 5;

then A25: t1 in dom h by A17, BORSUK_1:43;

A26: 0 in dom h by A24, BORSUK_1:43;

rng h = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def 5;

then h is onto by FUNCT_2:def 3;

then A27: h " = h " by A20, TOPS_2:def 4;

then (h ") . p1 = 0 by A14, A26, A20, FUNCT_1:32;

then A28: ((h ") * g) . 0 = 0 by A3, A23, FUNCT_1:13;

s1 in dom g by A6, A22, BORSUK_1:43;

then A29: ((h ") * g) . s1 = (h ") . q1 by A5, FUNCT_1:13

.= t1 by A16, A20, A25, A27, FUNCT_1:32 ;

A30: t2 in dom h by A19, A24, BORSUK_1:43;

s2 in dom g by A8, A22, BORSUK_1:43;

then A31: ((h ") * g) . s2 = (h ") . q2 by A7, FUNCT_1:13

.= t2 by A18, A20, A30, A27, FUNCT_1:32 ;

A32: 1 in dom g by A22, BORSUK_1:43;

A33: 1 in dom h by A24, BORSUK_1:43;

(h ") . p2 = 1 by A15, A33, A20, A27, FUNCT_1:32;

then A34: ((h ") * g) . 1 = 1 by A4, A32, FUNCT_1:13;

hence LE q1,q2,P,p1,p2 by A11, A12; :: thesis: verum