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 A1: ( LE q1,q2,p1,p2 & LE q2,q1,p1,p2 ) ; :: thesis: q1 = q2
then A2: ( q1 in LSeg p1,p2 & q2 in LSeg p1,p2 & ( for r1, r2 being Real st 0 <= r1 & r1 <= 1 & q1 = ((1 - r1) * p1) + (r1 * p2) & 0 <= r2 & r2 <= 1 & q2 = ((1 - r2) * p1) + (r2 * p2) holds
r1 <= r2 ) ) by Def6;
then consider r1 being Real such that
A3: ( q1 = ((1 - r1) * p1) + (r1 * p2) & 0 <= r1 & r1 <= 1 ) ;
consider r2 being Real such that
A4: ( q2 = ((1 - r2) * p1) + (r2 * p2) & 0 <= r2 & r2 <= 1 ) by A2;
A5: r1 <= r2 by A1, A3, A4, Def6;
r2 <= r1 by A1, A3, A4, Def6;
then r1 = r2 by A5, XXREAL_0:1;
hence q1 = q2 by A3, A4; :: thesis: verum