for F being Field
for V being VectSp of F
for A, B being finite Subset of V st B c= A holds
for v being Vector of V st v in Lin A & not v in Lin B holds
ex w being Vector of V st
( w in A \ B & w in Lin ((A \ {w}) \/ {v}) )