let n be 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 :: thesis: ( ( r2 <> 0 & ( p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) ) ) or ( r2 = 0 & ( p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) ) ) )
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, RLVECT_4:1;
then r2 * p3 = ((1 - r1) * p1) + ((r1 * p2) - ((1 - r2) * p2)) by RLVECT_1:def 3;
then (r2 ") * (r2 * p3) = (r2 ") * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2)) by RLVECT_1:35;
then ((r2 ") * r2) * p3 = (r2 ") * (((1 - r1) * p1) + ((r1 - (1 - r2)) * p2)) by RLVECT_1:def 7;
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 RLVECT_1:def 8
.= ((r2 ") * ((1 - r1) * p1)) + ((r2 ") * ((r1 - (1 - r2)) * p2)) by RLVECT_1:def 5
.= (((r2 ") * (1 - r1)) * p1) + ((r2 ") * ((r1 - (1 - r2)) * p2)) by RLVECT_1:def 7
.= (((r2 ") * (1 - r1)) * p1) + (((r2 ") * (r1 - (1 - r2))) * p2) by RLVECT_1:def 7 ;
r1 <= 1 + 0 by A6;
then r1 - 1 <= 0 by XREAL_1:20;
then (r1 - 1) + r2 <= 0 + r2 by XREAL_1:6;
then A12: (r2 ") * (r1 - (1 - r2)) <= (r2 ") * r2 by A8, XREAL_1:64;
((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:48;
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, RLVECT_1:10;
then p = p2 + (0. (TOP-REAL n)) by RLVECT_1:def 8;
hence ( p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) ) by A1, RLVECT_1:4; :: 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:6;
then A15: 1 - 1 <= 1 - r1 by XREAL_1:20;
A16: 0 + (1 - r2) <= (1 - (1 - r2)) + (1 - r2) by A8, XREAL_1:6;
now :: thesis: ( ( 1 - r1 <> 0 & ( p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) ) ) or ( 1 - r1 = 0 & ( p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) ) ) )
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, RLVECT_4:1
.= ((1 - (1 - r2)) * p3) + (((1 - r2) * p2) - ((1 - (1 - r1)) * p2)) by RLVECT_1:def 3
.= ((1 - (1 - r2)) * p3) + (((1 - r2) - (1 - (1 - r1))) * p2) by RLVECT_1:35 ;
then (((1 - r1) ") * (1 - r1)) * p1 = ((1 - r1) ") * (((1 - (1 - r2)) * p3) + (((1 - r2) - (1 - (1 - r1))) * p2)) by RLVECT_1:def 7;
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 RLVECT_1:def 8
.= (((1 - r1) ") * ((1 - (1 - r2)) * p3)) + (((1 - r1) ") * (((1 - r2) - (1 - (1 - r1))) * p2)) by RLVECT_1:def 5
.= ((((1 - r1) ") * (1 - (1 - r2))) * p3) + (((1 - r1) ") * (((1 - r2) - (1 - (1 - r1))) * p2)) by RLVECT_1:def 7 ;
then A18: p1 = ((((1 - r1) ") * (1 - (1 - r2))) * p3) + ((((1 - r1) ") * ((1 - r2) - (1 - (1 - r1)))) * p2) by RLVECT_1:def 7;
1 - r2 <= 1 + 0 by A16;
then (1 - r2) - 1 <= 0 by XREAL_1:20;
then ((1 - r2) - 1) + (1 - r1) <= 0 + (1 - r1) by XREAL_1:6;
then A19: ((1 - r1) ") * ((1 - r2) - (1 - (1 - r1))) <= ((1 - r1) ") * (1 - r1) by A15, XREAL_1:64;
(((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:48;
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, RLVECT_1:10;
then p = p2 + (0. (TOP-REAL n)) by RLVECT_1:def 8;
hence ( p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) ) by A1, RLVECT_1:4; :: thesis: verum
end;
end;
end;
hence ( p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) ) ; :: thesis: verum
end;
end;