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

set P = LSeg (p1,p2);

assume p1 <> p2 ; :: thesis: ( not LE q1,q2, LSeg (p1,p2),p1,p2 or LE q1,q2,p1,p2 )

then consider f being Function of I[01],((TOP-REAL 2) | (LSeg (p1,p2))) such that

A1: for x being Real st x in [.0,1.] holds

f . x = ((1 - x) * p1) + (x * p2) and

A2: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by JORDAN5A:3;

assume A3: LE q1,q2, LSeg (p1,p2),p1,p2 ; :: thesis: LE q1,q2,p1,p2

hence ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) ) ; :: according to JORDAN3:def 5 :: thesis: for b_{1}, b_{2} being object holds

( not 0 <= b_{1} or not b_{1} <= 1 or not q1 = ((1 - b_{1}) * p1) + (b_{1} * p2) or not 0 <= b_{2} or not b_{2} <= 1 or not q2 = ((1 - b_{2}) * p1) + (b_{2} * p2) or b_{1} <= b_{2} )

let r1, r2 be Real; :: thesis: ( not 0 <= r1 or not r1 <= 1 or not q1 = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not q2 = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 )

assume that

A4: 0 <= r1 and

A5: r1 <= 1 and

A6: q1 = ((1 - r1) * p1) + (r1 * p2) and

A7: ( 0 <= r2 & r2 <= 1 ) and

A8: q2 = ((1 - r2) * p1) + (r2 * p2) ; :: thesis: r1 <= r2

r2 in [.0,1.] by A7, BORSUK_1:40, BORSUK_1:43;

then A9: q2 = f . r2 by A8, A1;

r1 in [.0,1.] by A4, A5, BORSUK_1:40, BORSUK_1:43;

then q1 = f . r1 by A6, A1;

hence r1 <= r2 by A3, A5, A7, A2, A9; :: thesis: verum

set P = LSeg (p1,p2);

assume p1 <> p2 ; :: thesis: ( not LE q1,q2, LSeg (p1,p2),p1,p2 or LE q1,q2,p1,p2 )

then consider f being Function of I[01],((TOP-REAL 2) | (LSeg (p1,p2))) such that

A1: for x being Real st x in [.0,1.] holds

f . x = ((1 - x) * p1) + (x * p2) and

A2: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by JORDAN5A:3;

assume A3: LE q1,q2, LSeg (p1,p2),p1,p2 ; :: thesis: LE q1,q2,p1,p2

hence ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) ) ; :: according to JORDAN3:def 5 :: thesis: for b

( not 0 <= b

let r1, r2 be Real; :: thesis: ( not 0 <= r1 or not r1 <= 1 or not q1 = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not q2 = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 )

assume that

A4: 0 <= r1 and

A5: r1 <= 1 and

A6: q1 = ((1 - r1) * p1) + (r1 * p2) and

A7: ( 0 <= r2 & r2 <= 1 ) and

A8: q2 = ((1 - r2) * p1) + (r2 * p2) ; :: thesis: r1 <= r2

r2 in [.0,1.] by A7, BORSUK_1:40, BORSUK_1:43;

then A9: q2 = f . r2 by A8, A1;

r1 in [.0,1.] by A4, A5, BORSUK_1:40, BORSUK_1:43;

then q1 = f . r1 by A6, A1;

hence r1 <= r2 by A3, A5, A7, A2, A9; :: thesis: verum