theorem Th1: :: ANPROJ_2:1

for V being RealLinearSpace
for u, v, w being Element of V st ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) holds
( not u is zero & not v is zero & not w is zero & not u,v,w are_LinDep & not are_Prop u,v )