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