theorem Th17: :: RLVECT_5:17

for V being RealLinearSpace
for A being Subset of V st A is linearly-independent holds
for v being VECTOR of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B