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 A1: ( q1 in LSeg p1,p2 & q2 in LSeg p1,p2 & 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 ) )
then consider r1 being Real such that
A2: ( q1 = ((1 - r1) * p1) + (r1 * p2) & 0 <= r1 & r1 <= 1 ) ;
consider r2 being Real such that
A3: ( q2 = ((1 - r2) * p1) + (r2 * p2) & 0 <= r2 & r2 <= 1 ) by A1;

A4: now

per cases ( r1 <= r2 or r1 > r2 ) ;

case A5: 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 A6: ( 0 <= s1 & s1 <= 1 & q1 = ((1 - s1) * p1) + (s1 * p2) & 0 <= s2 & s2 <= 1 & q2 = ((1 - s2) * p1) + (s2 * p2) ) ; :: thesis: s1 <= s2
then ((1 - s1) * p1) + ((s1 * p2) - (s1 * p2)) = (((1 - r1) * p1) + (r1 * p2)) - (s1 * p2) by A2, EUCLID:49;
then ((1 - s1) * p1) + ((s1 * p2) - (s1 * p2)) = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by EUCLID:49;
then ((1 - s1) * p1) + (0. (TOP-REAL 2)) = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by EUCLID:46;
then (1 - s1) * p1 = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by EUCLID:31;
then (1 - s1) * p1 = ((1 - r1) * p1) + ((r1 - s1) * p2) by EUCLID:54;
then ((1 - s1) * p1) - ((1 - r1) * p1) = ((r1 - s1) * p2) + (((1 - r1) * p1) - ((1 - r1) * p1)) by EUCLID:49;
then ((1 - s1) * p1) - ((1 - r1) * p1) = ((r1 - s1) * p2) + (0. (TOP-REAL 2)) by EUCLID:46;
then ((1 - s1) * p1) - ((1 - r1) * p1) = (r1 - s1) * p2 by EUCLID:31;
then ((1 - s1) - (1 - r1)) * p1 = (r1 - s1) * p2 by EUCLID:54;
then A7: ( r1 - s1 = 0 or p1 = p2 ) by EUCLID:38;
((1 - s2) * p1) + ((s2 * p2) - (s2 * p2)) = (((1 - r2) * p1) + (r2 * p2)) - (s2 * p2) by A3, A6, EUCLID:49;
then ((1 - s2) * p1) + ((s2 * p2) - (s2 * p2)) = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by EUCLID:49;
then ((1 - s2) * p1) + (0. (TOP-REAL 2)) = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by EUCLID:46;
then (1 - s2) * p1 = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by EUCLID:31;
then (1 - s2) * p1 = ((1 - r2) * p1) + ((r2 - s2) * p2) by EUCLID:54;
then ((1 - s2) * p1) - ((1 - r2) * p1) = ((r2 - s2) * p2) + (((1 - r2) * p1) - ((1 - r2) * p1)) by EUCLID:49;
then ((1 - s2) * p1) - ((1 - r2) * p1) = ((r2 - s2) * p2) + (0. (TOP-REAL 2)) by EUCLID:46;
then ((1 - s2) * p1) - ((1 - r2) * p1) = (r2 - s2) * p2 by EUCLID:31;
then ((1 - s2) - (1 - r2)) * p1 = (r2 - s2) * p2 by EUCLID:54;
then ( r2 - s2 = 0 or p1 = p2 ) by EUCLID:38;
hence s1 <= s2 by A1, A5, A7; :: thesis: verum

end;

hence ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) by A1, Def6; :: thesis: verum

end;

case A8: 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 A9: ( 0 <= s2 & s2 <= 1 & q2 = ((1 - s2) * p1) + (s2 * p2) & 0 <= s1 & s1 <= 1 & q1 = ((1 - s1) * p1) + (s1 * p2) ) ; :: thesis: s1 >= s2
then ((1 - s1) * p1) + ((s1 * p2) - (s1 * p2)) = (((1 - r1) * p1) + (r1 * p2)) - (s1 * p2) by A2, EUCLID:49;
then ((1 - s1) * p1) + ((s1 * p2) - (s1 * p2)) = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by EUCLID:49;
then ((1 - s1) * p1) + (0. (TOP-REAL 2)) = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by EUCLID:46;
then (1 - s1) * p1 = ((1 - r1) * p1) + ((r1 * p2) - (s1 * p2)) by EUCLID:31;
then (1 - s1) * p1 = ((1 - r1) * p1) + ((r1 - s1) * p2) by EUCLID:54;
then ((1 - s1) * p1) - ((1 - r1) * p1) = ((r1 - s1) * p2) + (((1 - r1) * p1) - ((1 - r1) * p1)) by EUCLID:49;
then ((1 - s1) * p1) - ((1 - r1) * p1) = ((r1 - s1) * p2) + (0. (TOP-REAL 2)) by EUCLID:46;
then ((1 - s1) * p1) - ((1 - r1) * p1) = (r1 - s1) * p2 by EUCLID:31;
then ((1 - s1) - (1 - r1)) * p1 = (r1 - s1) * p2 by EUCLID:54;
then A10: ( r1 - s1 = 0 or p1 = p2 ) by EUCLID:38;
((1 - s2) * p1) + ((s2 * p2) - (s2 * p2)) = (((1 - r2) * p1) + (r2 * p2)) - (s2 * p2) by A3, A9, EUCLID:49;
then ((1 - s2) * p1) + ((s2 * p2) - (s2 * p2)) = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by EUCLID:49;
then ((1 - s2) * p1) + (0. (TOP-REAL 2)) = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by EUCLID:46;
then (1 - s2) * p1 = ((1 - r2) * p1) + ((r2 * p2) - (s2 * p2)) by EUCLID:31
.= ((r2 - s2) * p2) + ((1 - r2) * p1) by EUCLID:54 ;
then ((1 - s2) * p1) - ((1 - r2) * p1) = ((r2 - s2) * p2) + (((1 - r2) * p1) - ((1 - r2) * p1)) by EUCLID:49;
then ((1 - s2) * p1) - ((1 - r2) * p1) = ((r2 - s2) * p2) + (0. (TOP-REAL 2)) by EUCLID:46;
then ((1 - s2) * p1) - ((1 - r2) * p1) = (r2 - s2) * p2 by EUCLID:31;
then ((1 - s2) - (1 - r2)) * p1 = (r2 - s2) * p2 by EUCLID:54;
then ( r2 - s2 = 0 or p1 = p2 ) by EUCLID:38;
hence s1 >= s2 by A1, A8, A10; :: thesis: verum

end;

then ( LE q2,q1,p1,p2 & q1 <> q2 ) by A1, A2, A3, A8, Def6;
hence ( LE q1,q2,p1,p2 or LT q2,q1,p1,p2 ) by Def7; :: thesis: verum

end;

end;

end;

now

assume A11: ( LE q1,q2,p1,p2 & LT q2,q1,p1,p2 ) ; :: thesis: contradiction
then A12: r1 <= r2 by A2, A3, Def6;
( LE q2,q1,p1,p2 & q1 <> q2 ) by A11, Def7;
then r2 <= r1 by A2, A3, Def6;
then r1 = r2 by A12, XXREAL_0:1;
hence contradiction by A2, A3, A11, Def7; :: 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 A4; :: thesis: verum