theorem Th3: :: LMOD_6:3

for K being Ring
for V being LeftMod of K holds ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is strict Subspace of V