for R being Ring
for V being LeftMod of R
for x being set
for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds
x in W2 by VECTSP_4:8;