for V being RealLinearSpace
for u, v, w, y being VECTOR of V st u,v // w,y & u <> v & w <> y holds
ex a, b being Real st
( a * (v - u) = b * (y - w) & 0 < a & 0 < b ) ;