for V being RealLinearSpace
for p, q, u, v, w, y being VECTOR of V st p <> q & p,q // u,v & p,q // w,y holds
u,v // w,y