let V be RealLinearSpace; :: thesis: 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
let p, q, u, v, w, y be VECTOR of V; :: thesis: ( p <> q & p,q // u,v & p,q // w,y implies u,v // w,y )
assume that
A1: p <> q and
A2: p,q // u,v and
A3: p,q // w,y ; :: thesis: u,v // w,y

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

assume that
A4: u <> v and
A5: w <> y ; :: thesis: u,v // w,y
consider a, b being Real such that
A6: a * (q - p) = b * (v - u) and
A7: 0 < a and
A8: 0 < b by A1, A2, A4;
0 < a " by A7;
then A9: 0 < (a ") * b by A8, XREAL_1:129;
consider c, d being Real such that
A10: c * (q - p) = d * (y - w) and
A11: 0 < c and
A12: 0 < d by A1, A3, A5;
A13: q - p = (c ") * (d * (y - w)) by A10, A11, Th6
.= ((c ") * d) * (y - w) by RLVECT_1:def 7 ;
0 < c " by A11;
then A14: 0 < (c ") * d by A12, XREAL_1:129;
q - p = (a ") * (b * (v - u)) by A6, A7, Th6
.= ((a ") * b) * (v - u) by RLVECT_1:def 7 ;
hence u,v // w,y by A13, A9, A14; :: thesis: verum

end;

hence u,v // w,y ; :: thesis: verum