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 A4: ( u <> v & w <> y ) ; :: thesis: u,v // w,y
then consider a, b being Real such that
A5: ( a * (q - p) = b * (v - u) & 0 < a & 0 < b ) by A1, A2, Th16;
consider c, d being Real such that
A6: ( c * (q - p) = d * (y - w) & 0 < c & 0 < d ) by A1, A3, A4, Th16;
A7: q - p = (a " ) * (b * (v - u)) by A5, Th13
.= ((a " ) * b) * (v - u) by RLVECT_1:def 9 ;
A8: q - p = (c " ) * (d * (y - w)) by A6, Th13
.= ((c " ) * d) * (y - w) by RLVECT_1:def 9 ;
( 0 < a " & 0 < c " ) by A5, A6, XREAL_1:124;
then ( 0 < (a " ) * b & 0 < (c " ) * d ) by A5, A6, XREAL_1:131;
hence u,v // w,y by A7, A8, Def1; :: thesis: verum

end;

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