let a, b, c be Element of TarskiEuclid2Space; :: thesis: ( Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c)) implies ex jj being Real st
( 0 <= jj & jj <= 1 & (Tn2TR b) - (Tn2TR a) = jj * ((Tn2TR c) - (Tn2TR a)) ) )
assume Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c)) ; :: thesis: ex jj being Real st
( 0 <= jj & jj <= 1 & (Tn2TR b) - (Tn2TR a) = jj * ((Tn2TR c) - (Tn2TR a)) )
then consider jj being Real such that
G2: ( 0 <= jj & jj <= 1 & Tn2TR b = ((1 - jj) * (Tn2TR a)) + (jj * (Tn2TR c)) ) by RLTOPSP1:76;
set v = Tn2TR a;
set w = Tn2TR c;
(Tn2TR b) - (Tn2TR a) = (((1 - jj) * (Tn2TR a)) - (Tn2TR a)) + (jj * (Tn2TR c)) by RVSUM_1:15, G2
.= (((1 - jj) + (- 1)) * (Tn2TR a)) + (jj * (Tn2TR c)) by RVSUM_1:50
.= (jj * (Tn2TR c)) + ((jj * (- 1)) * (Tn2TR a))
.= (jj * (Tn2TR c)) + (jj * ((- 1) * (Tn2TR a))) by RVSUM_1:49
.= jj * ((Tn2TR c) - (Tn2TR a)) by RVSUM_1:51 ;
hence ex jj being Real st
( 0 <= jj & jj <= 1 & (Tn2TR b) - (Tn2TR a) = jj * ((Tn2TR c) - (Tn2TR a)) ) by G2; :: thesis: verum