let a, b, c, d, t be Element of TarskiEuclid2Space; :: thesis: ( between a,d,t & between b,d,c & a <> d implies ex x, y being Element of TarskiEuclid2Space st
( between a,b,x & between a,c,y & between x,t,y ) )
assume that
A1: between a,d,t and
A2: between b,d,c and
A3: a <> d ; :: thesis: ex x, y being Element of TarskiEuclid2Space st
( between a,b,x & between a,c,y & between x,t,y )
G0: Tn2TR d in LSeg ((Tn2TR a),(Tn2TR t)) by A1, ThConv6;
set v = Tn2TR a;
set w = Tn2TR t;
consider jj being Real such that
G2: ( 0 <= jj & jj <= 1 & Tn2TR d = ((1 - jj) * (Tn2TR a)) + (jj * (Tn2TR t)) ) by RLTOPSP1:76, G0;
g1: (Tn2TR d) - (Tn2TR a) = (((1 - jj) * (Tn2TR a)) - (Tn2TR a)) + (jj * (Tn2TR t)) by RVSUM_1:15, G2
.= (((1 - jj) + (- 1)) * (Tn2TR a)) + (jj * (Tn2TR t)) by RVSUM_1:50
.= (jj * (Tn2TR t)) + ((jj * (- 1)) * (Tn2TR a))
.= (jj * (Tn2TR t)) + (jj * ((- 1) * (Tn2TR a))) by RVSUM_1:49
.= jj * ((Tn2TR t) - (Tn2TR a)) by RVSUM_1:51 ;
set jt = 1 / jj;
JJ: jj <> 0
proof
assume jj = 0 ; :: thesis: contradiction
then (Tn2TR d) - (Tn2TR a) = 0. (TOP-REAL 2) by g1, RLVECT_1:10;
hence contradiction by A3, RLVECT_1:21; :: thesis: verum
end;
set xxx = ((1 / jj) * ((Tn2TR b) - (Tn2TR a))) + (Tn2TR a);
ww: MetrStruct(# the U1 of TarskiEuclid2Space, the distance of TarskiEuclid2Space #) = MetrStruct(# the U1 of (Euclid 2), the distance of (Euclid 2) #) by GTARSKI1:def 13;
then reconsider xx = ((1 / jj) * ((Tn2TR b) - (Tn2TR a))) + (Tn2TR a) as Element of TarskiEuclid2Space by EUCLID:22;
jj * ((((1 / jj) * ((Tn2TR b) - (Tn2TR a))) + (Tn2TR a)) - (Tn2TR a)) = jj * (((1 / jj) * ((Tn2TR b) - (Tn2TR a))) + ((Tn2TR a) - (Tn2TR a))) by RLVECT_1:28
.= jj * (((1 / jj) * ((Tn2TR b) - (Tn2TR a))) + (0. (TOP-REAL 2))) by RLVECT_1:15
.= (jj * (1 / jj)) * ((Tn2TR b) - (Tn2TR a)) by RLVECT_1:def 7
.= 1 * ((Tn2TR b) - (Tn2TR a)) by XCMPLX_0:def 7, JJ
.= (Tn2TR b) - (Tn2TR a) by RVSUM_1:52 ;
then Tn2TR b in LSeg ((Tn2TR a),(Tn2TR xx)) by G2, ThConvAGI;
then T1: between a,b,xx by ThConv6;
set yyy = ((1 / jj) * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a);
reconsider yy = ((1 / jj) * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a) as Element of TarskiEuclid2Space by ww, EUCLID:22;
jj * ((((1 / jj) * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a)) - (Tn2TR a)) = jj * (((1 / jj) * ((Tn2TR c) - (Tn2TR a))) + ((Tn2TR a) - (Tn2TR a))) by RLVECT_1:28
.= jj * (((1 / jj) * ((Tn2TR c) - (Tn2TR a))) + (0. (TOP-REAL 2))) by RLVECT_1:15
.= (jj * (1 / jj)) * ((Tn2TR c) - (Tn2TR a)) by RLVECT_1:def 7
.= 1 * ((Tn2TR c) - (Tn2TR a)) by XCMPLX_0:def 7, JJ
.= (Tn2TR c) - (Tn2TR a) by RVSUM_1:52 ;
then Tn2TR c in LSeg ((Tn2TR a),(Tn2TR yy)) by G2, ThConvAGI;
then T2: between a,c,yy by ThConv6;
Tn2TR d in LSeg ((Tn2TR b),(Tn2TR c)) by A2, ThConv6;
then consider kk being Real such that
Y1: ( 0 <= kk & kk <= 1 & (Tn2TR d) - (Tn2TR b) = kk * ((Tn2TR c) - (Tn2TR b)) ) by ThConvAG;
(1 / jj) * ((Tn2TR d) - (Tn2TR a)) = ((1 / jj) * jj) * ((Tn2TR t) - (Tn2TR a)) by g1, RLVECT_1:def 7
.= 1 * ((Tn2TR t) - (Tn2TR a)) by JJ, XCMPLX_0:def 7
.= (Tn2TR t) - (Tn2TR a) by RVSUM_1:52 ;
then w1: ((1 / jj) * ((Tn2TR d) - (Tn2TR a))) + (Tn2TR a) = (Tn2TR t) + ((- (Tn2TR a)) + (Tn2TR a)) by RLVECT_1:def 3
.= (Tn2TR t) + (0. (TOP-REAL 2)) by RLVECT_1:5 ;
W2: (Tn2TR yy) - (Tn2TR xx) = ((((1 / jj) * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a)) - (Tn2TR a)) - ((1 / jj) * ((Tn2TR b) - (Tn2TR a))) by RLVECT_1:27
.= (((1 / jj) * ((Tn2TR c) - (Tn2TR a))) + ((Tn2TR a) - (Tn2TR a))) - ((1 / jj) * ((Tn2TR b) - (Tn2TR a))) by RLVECT_1:28
.= (((1 / jj) * ((Tn2TR c) - (Tn2TR a))) + (0. (TOP-REAL 2))) - ((1 / jj) * ((Tn2TR b) - (Tn2TR a))) by RLVECT_1:15
.= (1 / jj) * (((Tn2TR c) - (Tn2TR a)) - ((Tn2TR b) - (Tn2TR a))) by RLVECT_1:34
.= (1 / jj) * ((Tn2TR c) - (Tn2TR b)) by ThWW ;
(Tn2TR t) - (Tn2TR xx) = ((((1 / jj) * ((Tn2TR d) - (Tn2TR a))) + (Tn2TR a)) - (Tn2TR a)) - ((1 / jj) * ((Tn2TR b) - (Tn2TR a))) by RLVECT_1:27, w1
.= (((1 / jj) * ((Tn2TR d) - (Tn2TR a))) + ((Tn2TR a) - (Tn2TR a))) - ((1 / jj) * ((Tn2TR b) - (Tn2TR a))) by RLVECT_1:def 3
.= (((1 / jj) * ((Tn2TR d) - (Tn2TR a))) + (0. (TOP-REAL 2))) - ((1 / jj) * ((Tn2TR b) - (Tn2TR a))) by RLVECT_1:5
.= (1 / jj) * (((Tn2TR d) - (Tn2TR a)) - ((Tn2TR b) - (Tn2TR a))) by RLVECT_1:34
.= (1 / jj) * ((Tn2TR d) - (Tn2TR b)) by ThWW
.= ((1 / jj) * kk) * ((Tn2TR c) - (Tn2TR b)) by RLVECT_1:def 7, Y1
.= kk * ((Tn2TR yy) - (Tn2TR xx)) by W2, RLVECT_1:def 7 ;
then Tn2TR t in LSeg ((Tn2TR xx),(Tn2TR yy)) by Y1, ThConvAGI;
then between xx,t,yy by ThConv6;
hence ex x, y being Element of TarskiEuclid2Space st
( between a,b,x & between a,c,y & between x,t,y ) by T1, T2; :: thesis: verum