theorem :: ZMODUL01:23

for V being Z_Module
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;