let V be RealLinearSpace; :: thesis: for p, u, v, w being VECTOR of V st p <> v & v,p // p,w holds
ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )

let p, u, v, w be VECTOR of V; :: thesis: ( p <> v & v,p // p,w implies ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) )

assume A1: ( p <> v & v,p // p,w ) ; :: thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )

A2: now :: thesis: ( p <> w implies ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) )
assume p <> w ; :: thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )

then consider a, b being Real such that
A3: a * (p - v) = b * (w - p) and
A4: 0 < a and
A5: 0 < b by A1;
set y = (((b ") * a) * (p - u)) + p;
A6: ((((b ") * a) * (p - u)) + p) - p = ((b ") * a) * (p - u) by RLSUB_2:61
.= (b ") * (a * (p - u)) by RLVECT_1:def 7 ;
A7: ((((b ") * a) * (p - u)) + p) - w = (((((b ") * a) * (p - u)) + p) - p) + (p - w) by Th1
.= (((((b ") * a) * (p - u)) + p) - p) - (w - p) by RLVECT_1:33 ;
v - u = (p - u) + (v - p) by Th1
.= (p - u) - (p - v) by RLVECT_1:33 ;
then a * (v - u) = (a * (p - u)) - (a * (p - v)) by RLVECT_1:34
.= (b * (((((b ") * a) * (p - u)) + p) - p)) - (b * (w - p)) by A3, A5, A6, Th6
.= b * (((((b ") * a) * (p - u)) + p) - w) by ;
then A8: u,v // w,(((b ") * a) * (p - u)) + p by A4, A5;
0 < b " by A5;
then A9: 0 < (b ") * a by ;
jj * (((((b ") * a) * (p - u)) + p) - p) = ((((b ") * a) * (p - u)) + p) - p by RLVECT_1:def 8
.= ((b ") * a) * (p - u) by RLSUB_2:61 ;
then u,p // p,(((b ") * a) * (p - u)) + p by A9;
hence ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) by A8; :: thesis: verum
end;
now :: thesis: ( p = w implies ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) )
assume A10: p = w ; :: thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )

take y = p; :: thesis: ( u,p // p,y & u,v // w,y )
thus ( u,p // p,y & u,v // w,y ) by A10; :: thesis: verum
end;
hence ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) by A2; :: thesis: verum