theorem Th54: :: ZMODUL01:54

for R being Ring
for V being LeftMod of R
for W being Submodule of V holds (0). V is Submodule of W by VECTSP_4:39;