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

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, Th16;
w - v = (w - u) + (u - v) by Th4
.= (w - u) - (v - u) by RLVECT_1:47 ;
then A5: a * (w - v) = (a * (w - u)) - (b * (w - u)) by A2, RLVECT_1:48
.= (a - b) * (w - u) by RLVECT_1:49
.= (b - a) * (u - w) by Th11 ;
v - w = (v - u) + (u - w) by Th4
.= (v - u) - (w - u) by RLVECT_1:47 ;
then A6: b * (v - w) = (b * (v - u)) - (a * (v - u)) by A2, RLVECT_1:48
.= (b - a) * (v - u) by RLVECT_1:49
.= (a - b) * (u - v) by Th11 ;

A7: now

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

end;

now

assume a = b ; :: thesis: ( u,v // v,w or u,w // w,v )
then (- u) + v = (- u) + w by A2, A3, RLVECT_1:50;
then v = w by RLVECT_1:21;
hence ( u,v // v,w or u,w // w,v ) by Def1; :: 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 ) by Def1; :: thesis: verum