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₁, b₂ being object holds
( not 0 <= b₁ or not b₁ <= 1 or not q1 = ((1 - b₁) * p1) + (b₁ * p2) or not 0 <= b₂ or not b₂ <= 1 or not q2 = ((1 - b₂) * p1) + (b₂ * p2) or b₁ <= 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