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 and
A3: 0 < b by ANALOAF:16;
take r = (a " ) * b; :: thesis: ( v - u = r * (w - v) & 0 < r )
0 < a " by A2, XREAL_1:124;
then A4: 0 * b < r by A3, XREAL_1:70;
v - u = 1 * (v - u) by RLVECT_1:def 11
.= ((a " ) * a) * (v - u) by A2, XCMPLX_0:def 7
.= (a " ) * (b * (w - v)) by A1, RLVECT_1:def 10
.= r * (w - v) by RLVECT_1:def 10 ;
hence ( v - u = r * (w - v) & 0 < r ) by A4; :: thesis: verum