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 A1: ( LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 ) ; :: thesis: LE q1,q3,P,p1,p2
then A2: ( q1 in P & q2 in P & ( 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 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) ) by Def3;
A3: ( q3 in P & ( 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 = q2 & 0 <= s1 & s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) ) by A1, Def3;

now

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 A4: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2
then A5: dom g = [#] I[01] by TOPS_2:def 5
.= the carrier of I[01] ;
rng g = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def 5
.= P by PRE_TOPC:def 10 ;
then consider x being set such that
A6: ( x in dom g & q2 = g . x ) by A2, FUNCT_1:def 5;
[.0 ,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def 1;
then consider s3 being Real such that
A7: ( s3 = x & 0 <= s3 & s3 <= 1 ) by A5, A6, BORSUK_1:83;
( s1 <= s3 & s3 <= s2 ) by A1, A4, A6, A7, Def3;
hence s1 <= s2 by XXREAL_0:2; :: thesis: verum

end;

hence LE q1,q3,P,p1,p2 by A2, A3, Def3; :: thesis: verum