let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( LE q1,q2,p1,p2 & LE q2,q1,p1,p2 implies q1 = q2 )
assume that
A1: LE q1,q2,p1,p2 and
A2: LE q2,q1,p1,p2 ; :: thesis: q1 = q2
q1 in LSeg (p1,p2) by A1;
then consider r1 being Real such that
A3: q1 = ((1 - r1) * p1) + (r1 * p2) and
A4: 0 <= r1 and
A5: r1 <= 1 ;
q2 in LSeg (p1,p2) by A1;
then consider r2 being Real such that
A6: q2 = ((1 - r2) * p1) + (r2 * p2) and
A7: 0 <= r2 and
A8: r2 <= 1 ;
A9: r2 <= r1 by A2, A3, A4, A5, A6, A8;
r1 <= r2 by A1, A3, A5, A6, A7, A8;
then r1 = r2 by A9, XXREAL_0:1;
hence q1 = q2 by A3, A6; :: thesis: verum