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

LE q1,q3,P,p1,p2

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

assume that

A1: LE q1,q2,P,p1,p2 and

A2: LE q2,q3,P,p1,p2 ; :: thesis: LE q1,q3,P,p1,p2

A3: q2 in P by A1;

hence LE q1,q3,P,p1,p2 by A4; :: thesis: verum

LE q1,q3,P,p1,p2

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

assume that

A1: LE q1,q2,P,p1,p2 and

A2: LE q2,q3,P,p1,p2 ; :: thesis: LE q1,q3,P,p1,p2

A3: q2 in P by A1;

A4: 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 = q3 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

( q1 in P & q3 in P )
by A1, A2;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 = q3 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

A5:
[.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) }
by RCOMP_1:def 1;

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 = q3 & 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 = q3 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )

assume that

A6: g is being_homeomorphism and

A7: ( g . 0 = p1 & g . 1 = p2 & g . s1 = q1 ) and

0 <= s1 and

A8: ( s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2

rng g = [#] ((TOP-REAL 2) | P) by A6, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

then consider x being object such that

A9: x in dom g and

A10: q2 = g . x by A3, FUNCT_1:def 3;

dom g = [#] I[01] by A6, TOPS_2:def 5

.= the carrier of I[01] ;

then consider s3 being Real such that

A11: ( s3 = x & 0 <= s3 & s3 <= 1 ) by A9, A5, BORSUK_1:40;

( s1 <= s3 & s3 <= s2 ) by A1, A2, A6, A7, A8, A10, A11;

hence s1 <= s2 by XXREAL_0:2; :: 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 = q3 & 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 = q3 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )

assume that

A6: g is being_homeomorphism and

A7: ( g . 0 = p1 & g . 1 = p2 & g . s1 = q1 ) and

0 <= s1 and

A8: ( s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2

rng g = [#] ((TOP-REAL 2) | P) by A6, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

then consider x being object such that

A9: x in dom g and

A10: q2 = g . x by A3, FUNCT_1:def 3;

dom g = [#] I[01] by A6, TOPS_2:def 5

.= the carrier of I[01] ;

then consider s3 being Real such that

A11: ( s3 = x & 0 <= s3 & s3 <= 1 ) by A9, A5, BORSUK_1:40;

( s1 <= s3 & s3 <= s2 ) by A1, A2, A6, A7, A8, A10, A11;

hence s1 <= s2 by XXREAL_0:2; :: thesis: verum

hence LE q1,q3,P,p1,p2 by A4; :: thesis: verum