let V be RealLinearSpace; :: thesis: ( ex p, q being VECTOR of V st p <> q implies for u, v, w being VECTOR of V ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
given p, q being VECTOR of V such that A1: p <> q ; :: thesis: for u, v, w being VECTOR of V ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
let u, v, w be VECTOR of V; :: thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )

A2: now

assume A3: u <> w ; :: thesis: ex y being M2(the carrier of V) ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
take y = (v + w) - u; :: thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )

A4: now

assume v = y ; :: thesis: contradiction
then v = v + (w - u) by RLVECT_1:def 6;
then w - u = 0. V by RLVECT_1:22;
hence contradiction by A3, RLVECT_1:35; :: thesis: verum

end;

( u,v // w,y & u,w // v,y ) by Th25;
hence ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A4; :: thesis: verum

end;

now

assume A5: u = w ; :: thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )

A6: now

assume u = v ; :: thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
then A7: ( u,v // w,p & u,v // w,q ) by Def1;
A8: ( v <> p or v <> q ) by A1;
( u,w // v,p & u,w // v,q ) by A5, Def1;
hence ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A8, A7; :: thesis: verum

end;

( u,v // w,u & u,w // v,u ) by A5, Def1;
hence ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A6; :: thesis: verum

end;

hence ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A2; :: thesis: verum