for R being non degenerated almost_left_invertible Ring
for V being LeftMod of R
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is base )