theorem Th15: :: RUSUB_3:15
for V being RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I