theorem Th109: :: ZMODUL01:109

for V being Z_Module
for W being strict Submodule of V holds ((Omega). V) /\ W = W by VECTSP_5:21;