theorem Th2: :: RLVECT_5:2

for V being RealLinearSpace
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I