let p0, p, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( p0 in LSeg (p,q1) & p0 in LSeg (p,q2) & p <> p0 & not q1 in LSeg (p,q2) implies q2 in LSeg (p,q1) )
assume that
A1: p0 in LSeg (p,q1) and
A2: p0 in LSeg (p,q2) and
A3: p <> p0 ; :: thesis: ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) )
consider r being Real such that
A4: p0 = ((1 - r) * p) + (r * q1) and
A5: 0 <= r and
A6: r <= 1 by A1;
A7: 1 - r >= 0 by A6, XREAL_1:48;
A8: p0 - (r * q1) = (1 - r) * p by A4, RLVECT_4:1;
consider s being Real such that
A9: p0 = ((1 - s) * p) + (s * q2) and
A10: 0 <= s and
A11: s <= 1 by A2;
A12: 1 - s >= 0 by A11, XREAL_1:48;
A13: p0 - (s * q2) = (1 - s) * p by A9, RLVECT_4:1;
A14: p0 - ((1 - s) * p) = s * q2 by A9, RLVECT_4:1;
A15: p0 - ((1 - r) * p) = r * q1 by A4, RLVECT_4:1;
A16: now :: thesis: ( r <> s & not q1 in LSeg (p,q2) implies q2 in LSeg (p,q1) )
assume A17: r <> s ; :: thesis: ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) )
now :: thesis: ( ( r < s & ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) ) ) or ( s < r & ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) ) ) )
per cases ( r < s or s < r ) by A17, XXREAL_0:1;
case A18: r < s ; :: thesis: ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) )
((1 - r) * p0) - ((1 - r) * ((1 - s) * p)) = (1 - r) * (s * q2) by A14, RLVECT_1:34;
then ((1 - r) * p0) - (((1 - r) * (1 - s)) * p) = (1 - r) * (s * q2) by RLVECT_1:def 7;
then ((1 - r) * p0) - (((1 - r) * (1 - s)) * p) = ((1 - r) * s) * q2 by RLVECT_1:def 7;
then ((1 - r) * p0) - ((1 - s) * ((1 - r) * p)) = ((1 - r) * s) * q2 by RLVECT_1:def 7;
then ((1 - r) * p0) - (((1 - s) * p0) - ((1 - s) * (r * q1))) = ((1 - r) * s) * q2 by A8, RLVECT_1:34;
then (((1 - r) * p0) - ((1 - s) * p0)) + ((1 - s) * (r * q1)) = ((1 - r) * s) * q2 by RLVECT_1:29;
then A19: (((1 - r) - (1 - s)) * p0) + ((1 - s) * (r * q1)) = ((1 - r) * s) * q2 by RLVECT_1:35;
A20: now :: thesis: not (1 - r) * s = 0
assume (1 - r) * s = 0 ; :: thesis: contradiction
then A21: ( (1 - r) + r = 0 + r or s = 0 ) by XCMPLX_1:6;
now :: thesis: ( ( r = 1 & contradiction ) or ( s = 0 & contradiction ) )
per cases ( r = 1 or s = 0 ) by A21;
end;
end;
hence contradiction ; :: thesis: verum
end;
then 1 = ((1 - r) * s) / ((1 - r) * s) by XCMPLX_1:60;
then 1 = ((1 - r) * s) * (((1 - r) * s) ") by XCMPLX_0:def 9;
then (((1 - r) * s) * (((1 - r) * s) ")) * (((s - r) * p0) + ((1 - s) * (r * q1))) = ((1 - r) * s) * q2 by A19, RLVECT_1:def 8;
then ((1 - r) * s) * ((((1 - r) * s) ") * (((s - r) * p0) + ((1 - s) * (r * q1)))) = ((1 - r) * s) * q2 by RLVECT_1:def 7;
then q2 = (((1 - r) * s) ") * (((s - r) * p0) + ((1 - s) * (r * q1))) by A20, RLVECT_1:36;
then q2 = (((1 - r) * s) ") * (((s - r) * p0) + (((1 - s) * r) * q1)) by RLVECT_1:def 7;
then q2 = ((((1 - r) * s) ") * ((s - r) * p0)) + ((((1 - r) * s) ") * (((1 - s) * r) * q1)) by RLVECT_1:def 5;
then q2 = (((((1 - r) * s) ") * (s - r)) * p0) + ((((1 - r) * s) ") * (((1 - s) * r) * q1)) by RLVECT_1:def 7;
then A22: q2 = (((((1 - r) * s) ") * (s - r)) * p0) + (((((1 - r) * s) ") * ((1 - s) * r)) * q1) by RLVECT_1:def 7;
set s1 = (((1 - r) * s) ") * ((1 - s) * r);
q1 in LSeg (p,q1) by RLTOPSP1:68;
then A23: LSeg (p0,q1) c= LSeg (p,q1) by A1, TOPREAL1:6;
(r - (s * r)) + (s * r) <= (s - (s * r)) + (s * r) by A18;
then (1 * r) - (s * r) <= (1 - r) * s by XREAL_1:6;
then (((1 - s) * r) / ((1 - r) * s)) * ((1 - r) * s) <= 1 * ((1 - r) * s) by A20, XCMPLX_1:87;
then ((1 - s) * r) / ((1 - r) * s) <= 1 by A10, A7, A20, XREAL_1:68;
then A24: (((1 - r) * s) ") * ((1 - s) * r) <= 1 by XCMPLX_0:def 9;
(((1 - r) * s) ") * (s - r) = (((1 - r) * s) - (((1 - r) * s) - (s - r))) / ((1 - r) * s) by XCMPLX_0:def 9
.= (((1 - r) * s) / ((1 - r) * s)) - ((((1 - r) * s) - (s - r)) / ((1 - r) * s)) by XCMPLX_1:120
.= 1 - (((r + (s - (r * s))) - s) / ((1 - r) * s)) by A20, XCMPLX_1:60
.= 1 - ((((1 - r) * s) ") * ((1 - s) * r)) by XCMPLX_0:def 9 ;
then q2 in LSeg (p0,q1) by A5, A10, A7, A12, A22, A24;
hence ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) ) by A23; :: thesis: verum
end;
case A25: s < r ; :: thesis: ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) )
((1 - s) * p0) - ((1 - s) * ((1 - r) * p)) = (1 - s) * (r * q1) by A15, RLVECT_1:34;
then ((1 - s) * p0) - (((1 - s) * (1 - r)) * p) = (1 - s) * (r * q1) by RLVECT_1:def 7;
then ((1 - s) * p0) - (((1 - s) * (1 - r)) * p) = ((1 - s) * r) * q1 by RLVECT_1:def 7;
then ((1 - s) * p0) - ((1 - r) * ((1 - s) * p)) = ((1 - s) * r) * q1 by RLVECT_1:def 7;
then ((1 - s) * p0) - (((1 - r) * p0) - ((1 - r) * (s * q2))) = ((1 - s) * r) * q1 by A13, RLVECT_1:34;
then (((1 - s) * p0) - ((1 - r) * p0)) + ((1 - r) * (s * q2)) = ((1 - s) * r) * q1 by RLVECT_1:29;
then A26: (((1 - s) - (1 - r)) * p0) + ((1 - r) * (s * q2)) = ((1 - s) * r) * q1 by RLVECT_1:35;
A27: now :: thesis: not (1 - s) * r = 0
assume (1 - s) * r = 0 ; :: thesis: contradiction
then A28: ( (1 - s) + s = 0 + s or r = 0 ) by XCMPLX_1:6;
now :: thesis: ( ( s = 1 & contradiction ) or ( r = 0 & contradiction ) )
per cases ( s = 1 or r = 0 ) by A28;
end;
end;
hence contradiction ; :: thesis: verum
end;
then 1 = ((1 - s) * r) / ((1 - s) * r) by XCMPLX_1:60;
then 1 = ((1 - s) * r) * (((1 - s) * r) ") by XCMPLX_0:def 9;
then (((1 - s) * r) * (((1 - s) * r) ")) * (((r - s) * p0) + ((1 - r) * (s * q2))) = ((1 - s) * r) * q1 by A26, RLVECT_1:def 8;
then ((1 - s) * r) * ((((1 - s) * r) ") * (((r - s) * p0) + ((1 - r) * (s * q2)))) = ((1 - s) * r) * q1 by RLVECT_1:def 7;
then q1 = (((1 - s) * r) ") * (((r - s) * p0) + ((1 - r) * (s * q2))) by A27, RLVECT_1:36;
then q1 = (((1 - s) * r) ") * (((r - s) * p0) + (((1 - r) * s) * q2)) by RLVECT_1:def 7;
then q1 = ((((1 - s) * r) ") * ((r - s) * p0)) + ((((1 - s) * r) ") * (((1 - r) * s) * q2)) by RLVECT_1:def 5;
then q1 = (((((1 - s) * r) ") * (r - s)) * p0) + ((((1 - s) * r) ") * (((1 - r) * s) * q2)) by RLVECT_1:def 7;
then A29: q1 = (((((1 - s) * r) ") * (r - s)) * p0) + (((((1 - s) * r) ") * ((1 - r) * s)) * q2) by RLVECT_1:def 7;
set s1 = (((1 - s) * r) ") * ((1 - r) * s);
q2 in LSeg (p,q2) by RLTOPSP1:68;
then A30: LSeg (p0,q2) c= LSeg (p,q2) by A2, TOPREAL1:6;
(s - (r * s)) + (r * s) <= (r - (r * s)) + (r * s) by A25;
then (1 * s) - (r * s) <= (1 - s) * r by XREAL_1:6;
then (((1 - r) * s) / ((1 - s) * r)) * ((1 - s) * r) <= 1 * ((1 - s) * r) by A27, XCMPLX_1:87;
then ((1 - r) * s) / ((1 - s) * r) <= 1 by A5, A12, A27, XREAL_1:68;
then A31: (((1 - s) * r) ") * ((1 - r) * s) <= 1 by XCMPLX_0:def 9;
(((1 - s) * r) ") * (r - s) = (((1 - s) * r) - (((1 - s) * r) - (r - s))) / ((1 - s) * r) by XCMPLX_0:def 9
.= (((1 - s) * r) / ((1 - s) * r)) - ((((1 - s) * r) - (r - s)) / ((1 - s) * r)) by XCMPLX_1:120
.= 1 - (((s + (r - (s * r))) - r) / ((1 - s) * r)) by A27, XCMPLX_1:60
.= 1 - ((((1 - s) * r) ") * ((1 - r) * s)) by XCMPLX_0:def 9 ;
then q1 in LSeg (p0,q2) by A5, A10, A7, A12, A29, A31;
hence ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) ) by A30; :: thesis: verum
end;
end;
end;
hence ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) ) ; :: thesis: verum
end;
now :: thesis: ( r = s & not q1 in LSeg (p,q2) implies q2 in LSeg (p,q1) )
assume r = s ; :: thesis: ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) )
then (r * q1) + (((1 - r) * p) - ((1 - r) * p)) = ((r * q2) + ((1 - r) * p)) - ((1 - r) * p) by A4, A9, RLVECT_1:def 3;
then (r * q1) + (0. (TOP-REAL 2)) = ((r * q2) + ((1 - r) * p)) - ((1 - r) * p) by RLVECT_1:5;
then (r * q1) + (0. (TOP-REAL 2)) = r * q2 by RLVECT_4:1;
then A32: r * q1 = r * q2 by RLVECT_1:4;
A33: q1 in LSeg (p,q1) by RLTOPSP1:68;
now :: thesis: ( ( r <> 0 & ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) ) ) or ( r = 0 & contradiction ) )
per cases ( r <> 0 or r = 0 ) ;
case r <> 0 ; :: thesis: ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) )
hence ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) ) by A32, A33, RLVECT_1:36; :: thesis: verum
end;
end;
end;
hence ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) ) ; :: thesis: verum
end;
hence ( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) ) by A16; :: thesis: verum