theorem Th12: :: RUSUB_3:12

for V being RealUnitarySpace
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )