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 A1: ( p1 <> p2 & 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 A1, RLTOPSP1:69; :: according to JORDAN3:def 6 :: thesis: for b₁, b₂ being Element of REAL 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 A2: ( 0 <= r1 & r1 <= 1 & p1 = ((1 - r1) * p1) + (r1 * p2) & 0 <= r2 & r2 <= 1 & p = ((1 - r2) * p1) + (r2 * p2) ) ; :: thesis: r1 <= r2
then 0. (TOP-REAL 2) = (((1 - r1) * p1) + (r1 * p2)) + (- p1) by EUCLID:40
.= (((1 - r1) * p1) + (r1 * p2)) - p1 by EUCLID:45
.= ((1 - r1) * p1) + ((r1 * p2) - p1) by EUCLID:49
.= ((1 - r1) * p1) + ((- p1) + (r1 * p2)) by EUCLID:45
.= (((1 - r1) * p1) + (- p1)) + (r1 * p2) by EUCLID:30
.= (((1 - r1) * p1) - p1) + (r1 * p2) by EUCLID:45 ;
then - (r1 * p2) = ((((1 - r1) * p1) - p1) + (r1 * p2)) + (- (r1 * p2)) by EUCLID:31
.= ((((1 - r1) * p1) - p1) + (r1 * p2)) - (r1 * p2) by EUCLID:45
.= (((1 - r1) * p1) - p1) + ((r1 * p2) - (r1 * p2)) by EUCLID:49
.= (((1 - r1) * p1) - p1) + (0. (TOP-REAL 2)) by EUCLID:46
.= ((1 - r1) * p1) - p1 by EUCLID:31
.= ((1 - r1) * p1) - (1 * p1) by EUCLID:33
.= ((1 - r1) - 1) * p1 by EUCLID:54
.= (- r1) * p1
.= - (r1 * p1) by EUCLID:44 ;
then r1 * p1 = - (- (r1 * p2)) by EUCLID:39
.= r1 * p2 by EUCLID:39 ;
hence r1 <= r2 by A1, A2, EUCLID:38; :: thesis: verum

end;