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 A1: p1 <> p2 ; :: thesis: ( not LE q1,q2, LSeg p1,p2,p1,p2 or LE q1,q2,p1,p2 )
assume A2: 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 ) by Def3; :: according to JORDAN3:def 6 :: thesis: for b₁, b₂ being Element of REAL 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 A3: ( 0 <= r1 & r1 <= 1 & q1 = ((1 - r1) * p1) + (r1 * p2) & 0 <= r2 & r2 <= 1 & q2 = ((1 - r2) * p1) + (r2 * p2) ) ; :: thesis: r1 <= r2
consider f being Function of I[01] ,((TOP-REAL 2) | (LSeg p1,p2)) such that
A4: ( ( for x being Real st x in [.0 ,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, JORDAN5A:4;
( r1 in [.0 ,1.] & r2 in [.0 ,1.] ) by A3, BORSUK_1:83, BORSUK_1:86;
then ( q1 = f . r1 & q2 = f . r2 ) by A3, A4;
hence r1 <= r2 by A2, A3, A4, Def3; :: thesis: verum