theorem :: ZMODUL01:51

for R being Ring
for V being LeftMod of R
for W being Submodule of V holds (0). W = (0). V by VECTSP_4:36;