let n be Element of NAT ; :: thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds
( for x being set holds
( not x <> p2 or not x in (LSeg p1,p2) /\ (LSeg p2,p3) ) or p1 in LSeg p2,p3 or p3 in LSeg p1,p2 )
let p1, p2, p3 be Point of (TOP-REAL n); :: thesis: ( for x being set holds
( not x <> p2 or not x in (LSeg p1,p2) /\ (LSeg p2,p3) ) or p1 in LSeg p2,p3 or p3 in LSeg p1,p2 )
given x being set such that A1: x <> p2 and
A2: x in (LSeg p1,p2) /\ (LSeg p2,p3) ; :: thesis: ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 )
reconsider p = x as Point of (TOP-REAL n) by A2;
A3: p in { (((1 - r1) * p1) + (r1 * p2)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by A2, XBOOLE_0:def 4;
A4: p in { (((1 - r2) * p2) + (r2 * p3)) where r2 is Real : ( 0 <= r2 & r2 <= 1 ) } by A2, XBOOLE_0:def 4;
consider r1 being Real such that
A5: p = ((1 - r1) * p1) + (r1 * p2) and
0 <= r1 and
A6: r1 <= 1 by A3;
consider r2 being Real such that
A7: p = ((1 - r2) * p2) + (r2 * p3) and
A8: 0 <= r2 and
r2 <= 1 by A4;
per cases ( r1 >= 1 - r2 or r1 < 1 - r2 ) ;
suppose A9: r1 >= 1 - r2 ; :: thesis: ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 )
now
per cases ( r2 <> 0 or r2 = 0 ) ;
case A10: r2 <> 0 ; :: thesis: ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 )
r2 * p3 = (((1 - r1) * p1) + (r1 * p2)) - ((1 - r2) * p2) by A5, A7, EUCLID:52;
then r2 * p3 = ((1 - r1) * p1) + ((r1 * p2) - ((1 - r2) * p2)) by EUCLID:49;
then (r2 " ) * (r2 * p3) = (r2 " ) * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2)) by EUCLID:54;
then ((r2 " ) * r2) * p3 = (r2 " ) * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2)) by EUCLID:34;
then 1 * p3 = (r2 " ) * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2)) by A10, XCMPLX_0:def 7;
then A11: p3 = (r2 " ) * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2)) by EUCLID:33
.= ((r2 " ) * ((1 - r1) * p1)) + ((r2 " ) * ((r1 - (1 - r2)) * p2)) by EUCLID:36
.= (((r2 " ) * (1 - r1)) * p1) + ((r2 " ) * ((r1 - (1 - r2)) * p2)) by EUCLID:34
.= (((r2 " ) * (1 - r1)) * p1) + (((r2 " ) * (r1 - (1 - r2))) * p2) by EUCLID:34 ;
r1 <= 1 + 0 by A6;
then r1 - 1 <= 0 by XREAL_1:22;
then (r1 - 1) + r2 <= 0 + r2 by XREAL_1:8;
then A12: (r2 " ) * (r1 - (1 - r2)) <= (r2 " ) * r2 by A8, XREAL_1:66;
((r2 " ) * (1 - r1)) + ((r2 " ) * (r1 - (1 - r2))) = (r2 " ) * ((1 - 1) + r2)
.= 1 by A10, XCMPLX_0:def 7 ;
then A13: (r2 " ) * (1 - r1) = 1 - ((r2 " ) * (r1 - (1 - r2))) ;
r1 - (1 - r2) >= 0 by A9, XREAL_1:50;
hence ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 ) by A8, A11, A13, A12; :: thesis: verum
end;
case r2 = 0 ; :: thesis: ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 )
then p = (1 * p2) + (0. (TOP-REAL n)) by A7, EUCLID:33;
then p = p2 + (0. (TOP-REAL n)) by EUCLID:33;
hence ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 ) by A1, EUCLID:31; :: thesis: verum
end;
end;
end;
hence ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 ) ; :: thesis: verum
end;
suppose A14: r1 < 1 - r2 ; :: thesis: ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 )
set s2 = 1 - r1;
set s1 = 1 - r2;
(1 - (1 - r1)) + (1 - r1) <= 1 + (1 - r1) by A6, XREAL_1:8;
then A15: 1 - 1 <= 1 - r1 by XREAL_1:22;
A16: 0 + (1 - r2) <= (1 - (1 - r2)) + (1 - r2) by A8, XREAL_1:8;
now
per cases ( 1 - r1 <> 0 or 1 - r1 = 0 ) ;
case A17: 1 - r1 <> 0 ; :: thesis: ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 )
(1 - r1) * p1 = (((1 - (1 - r2)) * p3) + ((1 - r2) * p2)) - ((1 - (1 - r1)) * p2) by A5, A7, EUCLID:52
.= ((1 - (1 - r2)) * p3) + (((1 - r2) * p2) - ((1 - (1 - r1)) * p2)) by EUCLID:49
.= ((1 - (1 - r2)) * p3) + (((1 - r2) - (1 - (1 - r1))) * p2) by EUCLID:54 ;
then (((1 - r1) " ) * (1 - r1)) * p1 = ((1 - r1) " ) * (((1 - (1 - r2)) * p3) + (((1 - r2) - (1 - (1 - r1))) * p2)) by EUCLID:34;
then 1 * p1 = ((1 - r1) " ) * (((1 - (1 - r2)) * p3) + (((1 - r2) - (1 - (1 - r1))) * p2)) by A17, XCMPLX_0:def 7;
then p1 = ((1 - r1) " ) * (((1 - (1 - r2)) * p3) + (((1 - r2) - (1 - (1 - r1))) * p2)) by EUCLID:33
.= (((1 - r1) " ) * ((1 - (1 - r2)) * p3)) + (((1 - r1) " ) * (((1 - r2) - (1 - (1 - r1))) * p2)) by EUCLID:36
.= ((((1 - r1) " ) * (1 - (1 - r2))) * p3) + (((1 - r1) " ) * (((1 - r2) - (1 - (1 - r1))) * p2)) by EUCLID:34 ;
then A18: p1 = ((((1 - r1) " ) * (1 - (1 - r2))) * p3) + ((((1 - r1) " ) * ((1 - r2) - (1 - (1 - r1)))) * p2) by EUCLID:34;
1 - r2 <= 1 + 0 by A16;
then (1 - r2) - 1 <= 0 by XREAL_1:22;
then ((1 - r2) - 1) + (1 - r1) <= 0 + (1 - r1) by XREAL_1:8;
then A19: ((1 - r1) " ) * ((1 - r2) - (1 - (1 - r1))) <= ((1 - r1) " ) * (1 - r1) by A15, XREAL_1:66;
(((1 - r1) " ) * (1 - (1 - r2))) + (((1 - r1) " ) * ((1 - r2) - (1 - (1 - r1)))) = ((1 - r1) " ) * ((1 - 1) + (1 - r1))
.= 1 by A17, XCMPLX_0:def 7 ;
then A20: ((1 - r1) " ) * (1 - (1 - r2)) = 1 - (((1 - r1) " ) * ((1 - r2) - (1 - (1 - r1)))) ;
(1 - r2) - (1 - (1 - r1)) >= 0 by A14, XREAL_1:50;
then p1 in { (((1 - r) * p3) + (r * p2)) where r is Real : ( 0 <= r & r <= 1 ) } by A15, A18, A20, A19;
hence ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 ) by RLTOPSP1:def 2; :: thesis: verum
end;
case 1 - r1 = 0 ; :: thesis: ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 )
then p = (1 * p2) + (0. (TOP-REAL n)) by A5, EUCLID:33;
then p = p2 + (0. (TOP-REAL n)) by EUCLID:33;
hence ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 ) by A1, EUCLID:31; :: thesis: verum
end;
end;
end;
hence ( p1 in LSeg p2,p3 or p3 in LSeg p1,p2 ) ; :: thesis: verum
end;
end;