let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (p1,p2) & p1 <> p2 implies LE p,p2,p1,p2 )
assume that
A1: p in LSeg (p1,p2) and
A2: p1 <> p2 ; :: thesis: LE p,p2,p1,p2
thus LE p,p2,p1,p2 :: thesis: verum

proof

thus ( p in LSeg (p1,p2) & p2 in LSeg (p1,p2) ) by A1, RLTOPSP1:68; :: according to JORDAN3:def 5 :: thesis: for b₁, b₂ being object holds
( not 0 <= b₁ or not b₁ <= 1 or not p = ((1 - b₁) * p1) + (b₁ * p2) or not 0 <= b₂ or not b₂ <= 1 or not p2 = ((1 - b₂) * p1) + (b₂ * p2) or b₁ <= b₂ )
let r1, r2 be Real; :: thesis: ( not 0 <= r1 or not r1 <= 1 or not p = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not p2 = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 )
assume that
0 <= r1 and
A3: r1 <= 1 and
p = ((1 - r1) * p1) + (r1 * p2) and
0 <= r2 and
r2 <= 1 and
A4: p2 = ((1 - r2) * p1) + (r2 * p2) ; :: thesis: r1 <= r2
p2 = 1 * p2 by RLVECT_1:def 8
.= (0. (TOP-REAL 2)) + (1 * p2) by RLVECT_1:4
.= ((1 - 1) * p1) + (1 * p2) by RLVECT_1:10 ;
hence r1 <= r2 by A2, A3, A4, JORDAN5A:2; :: thesis: verum

end;