theorem Th24: :: ZMODUL01:24

for V being Z_Module
for W being Submodule of V
for x being object st x in W holds
x in V by VECTSP_4:9;