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

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, Th16;
0 < a " by A7, XREAL_1:124;
then A9: 0 < (a " ) * b by A8, XREAL_1:131;
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, Th16;
A13: q - p = (c " ) * (d * (y - w)) by A10, A11, Th13
.= ((c " ) * d) * (y - w) by RLVECT_1:def 10 ;
0 < c " by A11, XREAL_1:124;
then A14: 0 < (c " ) * d by A12, XREAL_1:131;
q - p = (a " ) * (b * (v - u)) by A6, A7, Th13
.= ((a " ) * b) * (v - u) by RLVECT_1:def 10 ;
hence u,v // w,y by A13, A9, A14, Def1; :: thesis: verum

end;

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