let p0, p, q1, q2 be Point of (TOP-REAL 2); ( 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
; ( 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 ( r <> s & not q1 in LSeg (p,q2) implies q2 in LSeg (p,q1) )assume A17:
r <> s
;
( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) )now ( ( 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
;
( 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 not (1 - r) * s = 0 assume
(1 - r) * s = 0
;
contradictionthen A21:
(
(1 - r) + r = 0 + r or
s = 0 )
by XCMPLX_1:6;
now ( ( r = 1 & contradiction ) or ( s = 0 & contradiction ) )end; hence
contradiction
;
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;
verum end; case A25:
s < r
;
( 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 not (1 - s) * r = 0 assume
(1 - s) * r = 0
;
contradictionthen A28:
(
(1 - s) + s = 0 + s or
r = 0 )
by XCMPLX_1:6;
now ( ( s = 1 & contradiction ) or ( r = 0 & contradiction ) )end; hence
contradiction
;
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;
verum end; end; end; hence
(
q1 in LSeg (
p,
q2) or
q2 in LSeg (
p,
q1) )
;
verum end;
hence
( q1 in LSeg (p,q2) or q2 in LSeg (p,q1) )
by A16; verum