let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) & p1 <> p2 implies ( ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) & ( not LE q1,q2,p1,p2 or not LT q2,q1,p1,p2 ) ) )
assume that
A1: q1 in LSeg (p1,p2) and
A2: q2 in LSeg (p1,p2) and
A3: p1 <> p2 ; :: thesis: ( ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) & ( not LE q1,q2,p1,p2 or not LT q2,q1,p1,p2 ) )
consider r1 being Real such that
A4: q1 = ((1 - r1) * p1) + (r1 * p2) and
A5: 0 <= r1 and
A6: r1 <= 1 by A1;
consider r2 being Real such that
A7: q2 = ((1 - r2) * p1) + (r2 * p2) and
A8: 0 <= r2 and
A9: r2 <= 1 by A2;
A10: now :: thesis: ( ( r1 <= r2 & ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) ) or ( r1 > r2 & ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) ) )
per cases ( r1 <= r2 or r1 > r2 ) ;
case A11: r1 <= r2 ; :: thesis: ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 )
for s1, s2 being Real st 0 <= s1 & s1 <= 1 & q1 = ((1 - s1) * p1) + (s1 * p2) & 0 <= s2 & s2 <= 1 & q2 = ((1 - s2) * p1) + (s2 * p2) holds
s1 <= s2
proof
let s1, s2 be Real; :: thesis: ( 0 <= s1 & s1 <= 1 & q1 = ((1 - s1) * p1) + (s1 * p2) & 0 <= s2 & s2 <= 1 & q2 = ((1 - s2) * p1) + (s2 * p2) implies s1 <= s2 )
assume that
0 <= s1 and
s1 <= 1 and
A12: q1 = ((1 - s1) * p1) + (s1 * p2) and
0 <= s2 and
s2 <= 1 and
A13: q2 = ((1 - s2) * p1) + (s2 * p2) ; :: thesis: s1 <= s2
((1 - s2) * p1) + ((s2 * p2) - (s2 * p2)) = (((1 - r2) * p1) + (r2 * p2)) - (s2 * p2) by A7, A13, RLVECT_1:def 3;
then ((1 - s2) * p1) + ((s2 * p2) - (s2 * p2)) = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by RLVECT_1:def 3;
then ((1 - s2) * p1) + (0. (TOP-REAL 2)) = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by RLVECT_1:5;
then (1 - s2) * p1 = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by RLVECT_1:4;
then (1 - s2) * p1 = ((1 - r2) * p1) + ((r2 - s2) * p2) by RLVECT_1:35;
then ((1 - s2) * p1) - ((1 - r2) * p1) = ((r2 - s2) * p2) + (((1 - r2) * p1) - ((1 - r2) * p1)) by RLVECT_1:def 3;
then ((1 - s2) * p1) - ((1 - r2) * p1) = ((r2 - s2) * p2) + (0. (TOP-REAL 2)) by RLVECT_1:5;
then ((1 - s2) * p1) - ((1 - r2) * p1) = (r2 - s2) * p2 by RLVECT_1:4;
then ((1 - s2) - (1 - r2)) * p1 = (r2 - s2) * p2 by RLVECT_1:35;
then A14: ( r2 - s2 = 0 or p1 = p2 ) by RLVECT_1:36;
((1 - s1) * p1) + ((s1 * p2) - (s1 * p2)) = (((1 - r1) * p1) + (r1 * p2)) - (s1 * p2) by A4, A12, RLVECT_1:def 3;
then ((1 - s1) * p1) + ((s1 * p2) - (s1 * p2)) = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by RLVECT_1:def 3;
then ((1 - s1) * p1) + (0. (TOP-REAL 2)) = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by RLVECT_1:5;
then (1 - s1) * p1 = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by RLVECT_1:4;
then (1 - s1) * p1 = ((1 - r1) * p1) + ((r1 - s1) * p2) by RLVECT_1:35;
then ((1 - s1) * p1) - ((1 - r1) * p1) = ((r1 - s1) * p2) + (((1 - r1) * p1) - ((1 - r1) * p1)) by RLVECT_1:def 3;
then ((1 - s1) * p1) - ((1 - r1) * p1) = ((r1 - s1) * p2) + (0. (TOP-REAL 2)) by RLVECT_1:5;
then ((1 - s1) * p1) - ((1 - r1) * p1) = (r1 - s1) * p2 by RLVECT_1:4;
then ((1 - s1) - (1 - r1)) * p1 = (r1 - s1) * p2 by RLVECT_1:35;
then ( r1 - s1 = 0 or p1 = p2 ) by RLVECT_1:36;
hence s1 <= s2 by A3, A11, A14; :: thesis: verum
end;
hence ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) by A1, A2; :: thesis: verum
end;
case A15: r1 > r2 ; :: thesis: ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 )
for s2, s1 being Real st 0 <= s2 & s2 <= 1 & q2 = ((1 - s2) * p1) + (s2 * p2) & 0 <= s1 & s1 <= 1 & q1 = ((1 - s1) * p1) + (s1 * p2) holds
s1 >= s2
proof
let s2, s1 be Real; :: thesis: ( 0 <= s2 & s2 <= 1 & q2 = ((1 - s2) * p1) + (s2 * p2) & 0 <= s1 & s1 <= 1 & q1 = ((1 - s1) * p1) + (s1 * p2) implies s1 >= s2 )
assume that
0 <= s2 and
s2 <= 1 and
A16: q2 = ((1 - s2) * p1) + (s2 * p2) and
0 <= s1 and
s1 <= 1 and
A17: q1 = ((1 - s1) * p1) + (s1 * p2) ; :: thesis: s1 >= s2
((1 - s1) * p1) + ((s1 * p2) - (s1 * p2)) = (((1 - r1) * p1) + (r1 * p2)) - (s1 * p2) by A4, A17, RLVECT_1:def 3;
then ((1 - s1) * p1) + ((s1 * p2) - (s1 * p2)) = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by RLVECT_1:def 3;
then ((1 - s1) * p1) + (0. (TOP-REAL 2)) = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by RLVECT_1:5;
then (1 - s1) * p1 = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by RLVECT_1:4;
then (1 - s1) * p1 = ((1 - r1) * p1) + ((r1 - s1) * p2) by RLVECT_1:35;
then ((1 - s1) * p1) - ((1 - r1) * p1) = ((r1 - s1) * p2) + (((1 - r1) * p1) - ((1 - r1) * p1)) by RLVECT_1:def 3;
then ((1 - s1) * p1) - ((1 - r1) * p1) = ((r1 - s1) * p2) + (0. (TOP-REAL 2)) by RLVECT_1:5;
then ((1 - s1) * p1) - ((1 - r1) * p1) = (r1 - s1) * p2 by RLVECT_1:4;
then ((1 - s1) - (1 - r1)) * p1 = (r1 - s1) * p2 by RLVECT_1:35;
then A18: ( r1 - s1 = 0 or p1 = p2 ) by RLVECT_1:36;
((1 - s2) * p1) + ((s2 * p2) - (s2 * p2)) = (((1 - r2) * p1) + (r2 * p2)) - (s2 * p2) by A7, A16, RLVECT_1:def 3;
then ((1 - s2) * p1) + ((s2 * p2) - (s2 * p2)) = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by RLVECT_1:def 3;
then ((1 - s2) * p1) + (0. (TOP-REAL 2)) = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by RLVECT_1:5;
then (1 - s2) * p1 = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by RLVECT_1:4
.= ((r2 - s2) * p2) + ((1 - r2) * p1) by RLVECT_1:35 ;
then ((1 - s2) * p1) - ((1 - r2) * p1) = ((r2 - s2) * p2) + (((1 - r2) * p1) - ((1 - r2) * p1)) by RLVECT_1:def 3;
then ((1 - s2) * p1) - ((1 - r2) * p1) = ((r2 - s2) * p2) + (0. (TOP-REAL 2)) by RLVECT_1:5;
then ((1 - s2) * p1) - ((1 - r2) * p1) = (r2 - s2) * p2 by RLVECT_1:4;
then ((1 - s2) - (1 - r2)) * p1 = (r2 - s2) * p2 by RLVECT_1:35;
then ( r2 - s2 = 0 or p1 = p2 ) by RLVECT_1:36;
hence s1 >= s2 by A3, A15, A18; :: thesis: verum
end;
then A19: LE q2,q1,p1,p2 by A1, A2;
thus ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) by A19; :: thesis: verum
end;
end;
end;
now :: thesis: ( LE q1,q2,p1,p2 implies not LT q2,q1,p1,p2 )
assume that
A20: LE q1,q2,p1,p2 and
A21: LT q2,q1,p1,p2 ; :: thesis: contradiction
LE q2,q1,p1,p2 by A21;
then A22: r2 <= r1 by A4, A5, A6, A7, A9;
r1 <= r2 by A4, A6, A7, A8, A9, A20;
then r1 = r2 by A22, XXREAL_0:1;
hence contradiction by A4, A7, A21; :: thesis: verum
end;
hence ( ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) & ( not LE q1,q2,p1,p2 or not LT q2,q1,p1,p2 ) ) by A10; :: thesis: verum