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) & 0 < a & 0 < b ) by A1, Th16;
v - w = (v - u) + (u - w) by Th4
.= (v - u) - (w - u) by RLVECT_1:47 ;
then A3: 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 ;
w - v = (w - u) + (u - v) by Th4
.= (w - u) - (v - u) by RLVECT_1:47 ;
then A4: 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 ;

A5: now

assume a = b ; :: thesis: ( u,v // v,w or u,w // w,v )
then (- u) + v = (- u) + w by A2, 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;

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 A2, A3, A4, Def1;
hence ( u,v // v,w or u,w // w,v ) by Th21; :: thesis: verum

end;

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

end;

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