let V be RealLinearSpace; :: thesis: for u, v, w being VECTOR of V holds
( not u,v // u,w or u,v // v,w or u,w // w,v )
let u, v, w be VECTOR of V; :: thesis: ( not u,v // u,w or u,v // v,w or u,w // w,v )
assume A1: u,v // u,w ; :: thesis: ( u,v // v,w or u,w // w,v )

now :: thesis: ( u <> v & u <> w & not u,v // v,w implies u,w // w,v )

assume ( u <> v & u <> w ) ; :: thesis: ( u,v // v,w or u,w // w,v )
then consider a, b being Real such that
A2: a * (v - u) = b * (w - u) and
A3: 0 < a and
A4: 0 < b by A1;
w - v = (w - u) + (u - v) by Th1
.= (w - u) - (v - u) by RLVECT_1:33 ;
then A5: a * (w - v) = (a * (w - u)) - (b * (w - u)) by A2, RLVECT_1:34
.= (a - b) * (w - u) by RLVECT_1:35
.= (b - a) * (u - w) by Th4 ;
v - w = (v - u) + (u - w) by Th1
.= (v - u) - (w - u) by RLVECT_1:33 ;
then A6: b * (v - w) = (b * (v - u)) - (a * (v - u)) by A2, RLVECT_1:34
.= (b - a) * (v - u) by RLVECT_1:35
.= (a - b) * (u - v) by Th4 ;

A7: now :: thesis: ( not a <> b or u,v // v,w or u,w // w,v )

assume a <> b ; :: thesis: ( u,v // v,w or u,w // w,v )
then ( 0 < a - b or 0 < b - a ) by XREAL_1:55;
then ( v,u // w,v or w,u // v,w ) by A3, A4, A6, A5;
hence ( u,v // v,w or u,w // w,v ) by Th12; :: thesis: verum

end;

now :: thesis: ( not a = b or u,v // v,w or u,w // w,v )

assume a = b ; :: thesis: ( u,v // v,w or u,w // w,v )
then (- u) + v = (- u) + w by A2, A3, RLVECT_1:36;
then v = w by RLVECT_1:8;
hence ( u,v // v,w or u,w // w,v ) ; :: thesis: verum

end;

hence ( u,v // v,w or u,w // w,v ) by A7; :: thesis: verum

end;

hence ( u,v // v,w or u,w // w,v ) ; :: thesis: verum