theorem :: ZMODUL01:103

for V being Z_Module
for W being strict Submodule of V holds W /\ W = W by VECTSP_5:13;