theorem :: VECTSP_7:27
for R being domRing
for V being strict LeftMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V