theorem ThLin4: :: ZMODUL05:30
for R being Ring
for V being LeftMod of R
for A being Subset of V holds A is Subset of (Lin A)