theorem :: ZMODUL01:44

for R being Ring
for V being LeftMod of R
for W1, W2 being Submodule of V st ( for v being Vector of V st v in W1 holds
v in W2 ) holds
W1 is Submodule of W2 by VECTSP_4:28;