theorem Th3: :: ANPROJ_2:3

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