theorem Th20: :: ANALOAF:20

for V being RealLinearSpace st ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) holds
ex u, v, w, y being VECTOR of V st
( not u,v // w,y & not u,v // y,w )