let q1, q2, p1, p2 be Point of (TOP-REAL 2); ( p1 <> p2 & LE q1,q2, LSeg (p1,p2),p1,p2 implies LE q1,q2,p1,p2 )
set P = LSeg (p1,p2);
assume
p1 <> p2
; ( 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
; LE q1,q2,p1,p2
hence
( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) )
; JORDAN3:def 5 for b1, b2 being object holds
( not 0 <= b1 or not b1 <= 1 or not q1 = ((1 - b1) * p1) + (b1 * p2) or not 0 <= b2 or not b2 <= 1 or not q2 = ((1 - b2) * p1) + (b2 * p2) or b1 <= b2 )
let r1, r2 be Real; ( 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)
; 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; verum