let n be Nat; 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); ( 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))
; ( 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
;
( p1 in LSeg (p2,p3) or p3 in LSeg (p1,p2) )now ( ( 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
;
( 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;
verum end; end; end; hence
(
p1 in LSeg (
p2,
p3) or
p3 in LSeg (
p1,
p2) )
;
verum end; suppose A14:
r1 < 1
- r2
;
( 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 ( ( 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
;
( 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;
verum end; end; end; hence
(
p1 in LSeg (
p2,
p3) or
p3 in LSeg (
p1,
p2) )
;
verum end; end;