let V be RealLinearSpace; :: thesis: for u, v, w being VECTOR of V st u <> v & w <> v & u,v // v,w holds
ex r being Real st
( v - u = r * (w - v) & 0 < r )
let u, v, w be VECTOR of V; :: thesis: ( u <> v & w <> v & u,v // v,w implies ex r being Real st
( v - u = r * (w - v) & 0 < r ) )
assume ( u <> v & w <> v & u,v // v,w ) ; :: thesis: ex r being Real st
( v - u = r * (w - v) & 0 < r )
then consider a, b being Real such that
A1: a * (v - u) = b * (w - v) and
A2: ( 0 < a & 0 < b ) by ANALOAF:16;
take r = (a " ) * b; :: thesis: ( v - u = r * (w - v) & 0 < r )
A3: 0 < r

proof

0 < a " by A2, XREAL_1:124;
then 0 * b < r by A2, XREAL_1:70;
hence 0 < r ; :: thesis: verum

end;

v - u = 1 * (v - u) by RLVECT_1:def 9
.= ((a " ) * a) * (v - u) by A2, XCMPLX_0:def 7
.= (a " ) * (b * (w - v)) by A1, RLVECT_1:def 9
.= r * (w - v) by RLVECT_1:def 9 ;
hence ( v - u = r * (w - v) & 0 < r ) by A3; :: thesis: verum