for V being RealLinearSpace
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A