theorem :: GTARSKI2:43

for n being Nat
for a, b, c being Element of (TarskiEuclidSpace n) st Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c)) holds
ex jj being Real st
( 0 <= jj & jj <= 1 & (Tn2TR b) - (Tn2TR a) = jj * ((Tn2TR c) - (Tn2TR a)) )