theorem :: ZMODUL01:52

for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds (0). W1 = (0). W2 by VECTSP_4:37;