for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V holds 0. W1 in W2 by VECTSP_4:18;