theorem :: ZMODUL01:51

for V being Z_Module
for W being Submodule of V holds (0). W = (0). V by VECTSP_4:36;