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