theorem :: LMOD_6:10

for x being set
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds
( x in @ ([#] W) iff x in W ) ;