let P be Subset of (); :: thesis: for p1, p2, q1 being Point of () 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 (); :: 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 () by A2;
A3: now :: thesis: for g being Function of I,(() | 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
A4: 0 in the carrier of I by BORSUK_1:43;
let g be Function of I,(() | 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 & g is one-to-one ) by ;
hence s1 <= s2 by ; :: thesis: verum
end;
A10: now :: thesis: for g being Function of I,(() | 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
A11: 1 in the carrier of I by BORSUK_1:43;
let g be Function of I,(() | 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 & g is one-to-one ) by ;
hence s1 <= s2 by ; :: thesis: verum
end;
( p1 in P & p2 in P ) by ;
hence ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) by A2, A3, A10; :: thesis: verum