theorem Th25: :: RUSUB_3:25

for V being RealUnitarySpace
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