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 :: thesis: ( u <> w implies ex y being M3( the carrier of V) ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
assume A3: u <> w ; :: thesis: ex y being M3( 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 :: thesis: not v = yend;
( u,v // w,y & u,w // v,y ) by Th16;
hence ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) by A4; :: thesis: verum
end;
now :: thesis: ( u = w implies ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
assume A5: u = w ; :: thesis: ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )

A6: now :: thesis: ( u = v implies ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
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 ) ;
A8: ( v <> p or v <> q ) by A1;
( u,w // v,p & u,w // v,q ) by A5;
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;
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