theorem Th42: :: ZMODUL01:42

for V, X, Y being Z_Module st V is Submodule of X & X is Submodule of Y holds
V is Submodule of Y by VECTSP_4:26;