:: deftheorem defines @ LMOD_6:def 2 :
for K being Ring
for V being LeftMod of K
for W being strict Subspace of V holds @ W = W;