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

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) & 0 < a & 0 < b ) by A1, Th16;
a * (u - v) = - (b * (y - w)) by A2, Th10
.= b * (w - y) by Th10 ;
hence ( v,u // y,w & w,y // u,v ) by A2, Def1; :: thesis: verum

end;

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