let p, q, p1, p2 be Point of (TOP-REAL 2); ( LE p,q,p1,p2 implies ( q in LSeg (p,p2) & p in LSeg (p1,q) ) )
assume A1:
LE p,q,p1,p2
; ( q in LSeg (p,p2) & p in LSeg (p1,q) )
then
p in LSeg (p1,p2)
;
then consider s1 being Real such that
A2:
p = ((1 - s1) * p1) + (s1 * p2)
and
A3:
0 <= s1
and
A4:
s1 <= 1
;
q in LSeg (p1,p2)
by A1;
then consider s2 being Real such that
A5:
q = ((1 - s2) * p1) + (s2 * p2)
and
A6:
0 <= s2
and
A7:
s2 <= 1
;
A8:
s1 <= s2
by A1, A2, A4, A5, A6, A7;
A9:
1 - s1 >= 0
by A4, XREAL_1:48;
A10:
now ( ( 1 - s1 <> 0 & q in LSeg (p,p2) ) or ( 1 - s1 = 0 & q in LSeg (p,p2) ) )per cases
( 1 - s1 <> 0 or 1 - s1 = 0 )
;
case A11:
1
- s1 <> 0
;
q in LSeg (p,p2)set s =
(s2 - s1) / (1 - s1);
A12:
(1 - s1) * ((1 - s2) / (1 - s1)) = 1
- s2
by A11, XCMPLX_1:87;
A13:
(1 - s1) * ((s2 - s1) / (1 - s1)) = s2 - s1
by A11, XCMPLX_1:87;
1
- ((s2 - s1) / (1 - s1)) =
((1 * (1 - s1)) - (s2 - s1)) / (1 - s1)
by A11, XCMPLX_1:127
.=
(((1 - s1) + s1) - s2) / (1 - s1)
;
then (1 - s1) * (((1 - ((s2 - s1) / (1 - s1))) * p) + (((s2 - s1) / (1 - s1)) * p2)) =
((1 - s1) * (((1 - s2) / (1 - s1)) * (((1 - s1) * p1) + (s1 * p2)))) + ((1 - s1) * (((s2 - s1) / (1 - s1)) * p2))
by A2, RLVECT_1:def 5
.=
(((1 - s1) * ((1 - s2) / (1 - s1))) * (((1 - s1) * p1) + (s1 * p2))) + ((1 - s1) * (((s2 - s1) / (1 - s1)) * p2))
by RLVECT_1:def 7
.=
((1 - s2) * (((1 - s1) * p1) + (s1 * p2))) + (((1 - s1) * ((s2 - s1) / (1 - s1))) * p2)
by A12, RLVECT_1:def 7
.=
(((1 - s2) * ((1 - s1) * p1)) + ((1 - s2) * (s1 * p2))) + ((s2 - s1) * p2)
by A13, RLVECT_1:def 5
.=
((((1 - s2) * (1 - s1)) * p1) + ((1 - s2) * (s1 * p2))) + ((s2 - s1) * p2)
by RLVECT_1:def 7
.=
((((1 - s2) * (1 - s1)) * p1) + (((1 - s2) * s1) * p2)) + ((s2 - s1) * p2)
by RLVECT_1:def 7
.=
(((1 - s2) * (1 - s1)) * p1) + ((((1 - s2) * s1) * p2) + ((s2 - s1) * p2))
by RLVECT_1:def 3
.=
(((1 - s2) * (1 - s1)) * p1) + ((((1 * s1) - (s2 * s1)) + (s2 - s1)) * p2)
by RLVECT_1:def 6
.=
((1 - s1) * ((1 - s2) * p1)) + (((1 - s1) * s2) * p2)
by RLVECT_1:def 7
.=
((1 - s1) * ((1 - s2) * p1)) + ((1 - s1) * (s2 * p2))
by RLVECT_1:def 7
.=
(1 - s1) * q
by A5, RLVECT_1:def 5
;
then A14:
q = ((1 - ((s2 - s1) / (1 - s1))) * p) + (((s2 - s1) / (1 - s1)) * p2)
by A11, RLVECT_1:36;
1
- s1 >= s2 - s1
by A7, XREAL_1:9;
then
(1 - s1) / (1 - s1) >= (s2 - s1) / (1 - s1)
by A9, XREAL_1:72;
then A15:
1
>= (s2 - s1) / (1 - s1)
by A11, XCMPLX_1:60;
s2 - s1 >= 0
by A8, XREAL_1:48;
hence
q in LSeg (
p,
p2)
by A9, A15, A14;
verum end; end; end;
now ( ( s2 <> 0 & p in LSeg (p1,q) ) or ( s2 = 0 & p in LSeg (p1,q) ) )per cases
( s2 <> 0 or s2 = 0 )
;
case A16:
s2 <> 0
;
p in LSeg (p1,q)set s =
s1 / s2;
s2 / s2 >= s1 / s2
by A6, A8, XREAL_1:72;
then A17:
1
>= s1 / s2
by A16, XCMPLX_1:60;
A18:
(s2 - s1) + (s1 * (1 - s2)) = s2 * (1 - s1)
;
A19:
s2 * (s1 / s2) = s1
by A16, XCMPLX_1:87;
A20:
s2 * ((s2 - s1) / s2) = s2 - s1
by A16, XCMPLX_1:87;
s2 * (((1 - (s1 / s2)) * p1) + ((s1 / s2) * q)) =
s2 * (((((1 * s2) - s1) / s2) * p1) + ((s1 / s2) * (((1 - s2) * p1) + (s2 * p2))))
by A5, A16, XCMPLX_1:127
.=
(s2 * (((s2 - s1) / s2) * p1)) + (s2 * ((s1 / s2) * (((1 - s2) * p1) + (s2 * p2))))
by RLVECT_1:def 5
.=
((s2 * ((s2 - s1) / s2)) * p1) + (s2 * ((s1 / s2) * (((1 - s2) * p1) + (s2 * p2))))
by RLVECT_1:def 7
.=
((s2 - s1) * p1) + ((s2 * (s1 / s2)) * (((1 - s2) * p1) + (s2 * p2)))
by A20, RLVECT_1:def 7
.=
((s2 - s1) * p1) + ((s1 * ((1 - s2) * p1)) + (s1 * (s2 * p2)))
by A19, RLVECT_1:def 5
.=
((s2 - s1) * p1) + (((s1 * (1 - s2)) * p1) + (s1 * (s2 * p2)))
by RLVECT_1:def 7
.=
((s2 - s1) * p1) + (((s1 * (1 - s2)) * p1) + ((s1 * s2) * p2))
by RLVECT_1:def 7
.=
(((s2 - s1) * p1) + ((s1 * (1 - s2)) * p1)) + ((s1 * s2) * p2)
by RLVECT_1:def 3
.=
(((s2 - s1) + (s1 * (1 - s2))) * p1) + ((s1 * s2) * p2)
by RLVECT_1:def 6
.=
(s2 * ((1 - s1) * p1)) + ((s2 * s1) * p2)
by A18, RLVECT_1:def 7
.=
(s2 * ((1 - s1) * p1)) + (s2 * (s1 * p2))
by RLVECT_1:def 7
.=
s2 * p
by A2, RLVECT_1:def 5
;
then
p = ((1 - (s1 / s2)) * p1) + ((s1 / s2) * q)
by A16, RLVECT_1:36;
hence
p in LSeg (
p1,
q)
by A3, A6, A17;
verum end; end; end;
hence
( q in LSeg (p,p2) & p in LSeg (p1,q) )
by A10; verum