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

proof

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

end;