for V being RealLinearSpace
for p, q, r, s being Element of V st ( for w being Element of V ex a, b, c, d being Real st w = (((a * p) + (b * q)) + (c * r)) + (d * s) ) & ( for a, b, c, d being Real st (((a * p) + (b * q)) + (c * r)) + (d * s) = 0. V holds
( a = 0 & b = 0 & c = 0 & d = 0 ) ) holds
for u, v being Element of V st not u is zero & not v is zero holds
ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & not y is zero & not w is zero )