theorem Th25: :: RLVECT_3:25

for V being RealLinearSpace
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 )