let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P holds

( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & q1 in P implies ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) )

assume that

A1: P is_an_arc_of p1,p2 and

A2: q1 in P ; :: thesis: ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )

reconsider P = P as non empty Subset of (TOP-REAL 2) by A2;

hence ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) by A2, A3, A10; :: thesis: verum

( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & q1 in P implies ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) )

assume that

A1: P is_an_arc_of p1,p2 and

A2: q1 in P ; :: thesis: ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )

reconsider P = P as non empty Subset of (TOP-REAL 2) by A2;

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

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

s1 <= s2

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

s1 <= s2

A4:
0 in the carrier of I[01]
by BORSUK_1:43;

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

s1 <= s2

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

assume that

A5: g is being_homeomorphism and

A6: g . 0 = p1 and

g . 1 = p2 and

A7: g . s1 = p1 and

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

g . s2 = q1 and

A9: 0 <= s2 and

s2 <= 1 ; :: thesis: s1 <= s2

( s1 in the carrier of I[01] & g is one-to-one ) by A5, A8, BORSUK_1:43, TOPS_2:def 5;

hence s1 <= s2 by A6, A7, A9, A4, FUNCT_2:19; :: thesis: verum

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

s1 <= s2

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

assume that

A5: g is being_homeomorphism and

A6: g . 0 = p1 and

g . 1 = p2 and

A7: g . s1 = p1 and

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

g . s2 = q1 and

A9: 0 <= s2 and

s2 <= 1 ; :: thesis: s1 <= s2

( s1 in the carrier of I[01] & g is one-to-one ) by A5, A8, BORSUK_1:43, TOPS_2:def 5;

hence s1 <= s2 by A6, A7, A9, A4, FUNCT_2:19; :: thesis: verum

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

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

s1 <= s2

( p1 in P & p2 in P )
by A1, TOPREAL1:1;for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

A11:
1 in the carrier of I[01]
by BORSUK_1:43;

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

s1 <= s2

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

assume that

A12: g is being_homeomorphism and

g . 0 = p1 and

A13: g . 1 = p2 and

g . s1 = q1 and

0 <= s1 and

A14: ( s1 <= 1 & g . s2 = p2 ) and

A15: ( 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2

( s2 in the carrier of I[01] & g is one-to-one ) by A12, A15, BORSUK_1:43, TOPS_2:def 5;

hence s1 <= s2 by A13, A14, A11, FUNCT_2:19; :: thesis: verum

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

s1 <= s2

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

assume that

A12: g is being_homeomorphism and

g . 0 = p1 and

A13: g . 1 = p2 and

g . s1 = q1 and

0 <= s1 and

A14: ( s1 <= 1 & g . s2 = p2 ) and

A15: ( 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2

( s2 in the carrier of I[01] & g is one-to-one ) by A12, A15, BORSUK_1:43, TOPS_2:def 5;

hence s1 <= s2 by A13, A14, A11, FUNCT_2:19; :: thesis: verum

hence ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) by A2, A3, A10; :: thesis: verum