let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st u,v // w,y holds
( v,u // y,w & w,y // u,v )
let u, v, w, y be VECTOR of V; :: thesis: ( u,v // w,y implies ( v,u // y,w & w,y // u,v ) )
assume A1: u,v // w,y ; :: thesis: ( v,u // y,w & w,y // u,v )

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

assume ( u <> v & w <> y ) ; :: thesis: ( v,u // y,w & w,y // u,v )
then consider a, b being Real such that
A2: a * (v - u) = b * (y - w) and
A3: ( 0 < a & 0 < b ) by A1;
a * (u - v) = - (b * (y - w)) by A2, Th3
.= b * (w - y) by Th3 ;
hence ( v,u // y,w & w,y // u,v ) by A2, A3; :: thesis: verum

end;

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