for V being RealLinearSpace
for p, q, u, v, w being Element of V st not u,v,w are_LinDep & u,v,p are_LinDep & v,w,q are_LinDep holds
ex y being Element of V st
( u,w,y are_LinDep & p,q,y are_LinDep & not y is zero )