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 VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
then A4: ( u,v // w,u & u,w // v,u ) by Def1;

now

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

end;

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 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 )
A6: ( u,v // w,y & u,w // v,y ) by Th25;

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 A5, RLVECT_1:35; :: thesis: verum

end;

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