let p1, p2, p be Point of (TOP-REAL 2); :: thesis: ( p1 <> p2 & p in LSeg (p1,p2) implies LE p,p,p1,p2 )
assume that
A1: p1 <> p2 and
A2: p in LSeg (p1,p2) ; :: thesis: LE p,p,p1,p2
thus LE p,p,p1,p2 :: thesis: verum
proof
thus ( p in LSeg (p1,p2) & p in LSeg (p1,p2) ) by A2; :: according to JORDAN3:def 5 :: thesis: for b1, b2 being Element of REAL holds
( not 0 <= b1 or not b1 <= 1 or not p = ((1 - b1) * p1) + (b1 * p2) or not 0 <= b2 or not b2 <= 1 or not p = ((1 - b2) * p1) + (b2 * p2) or b1 <= b2 )
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 p = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 )
assume that
0 <= r1 and
r1 <= 1 and
A3: p = ((1 - r1) * p1) + (r1 * p2) and
0 <= r2 and
r2 <= 1 and
A4: p = ((1 - r2) * p1) + (r2 * p2) ; :: thesis: r1 <= r2
thus r1 <= r2 by A1, A3, A4, JORDAN5A:2; :: thesis: verum
end;