theorem Th21: :: ANALOAF:21

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