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 A1: ( p1 <> p2 & 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 A1; :: according to JORDAN3:def 6 :: 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 ( 0 <= r1 & r1 <= 1 & p = ((1 - r1) * p1) + (r1 * p2) & 0 <= r2 & r2 <= 1 & p = ((1 - r2) * p1) + (r2 * p2) ) ; :: thesis: r1 <= r2
hence r1 <= r2 by A1, JORDAN5A:3; :: thesis: verum
end;