theorem Th46: :: ZMODUL01:46

for R being Ring
for V being LeftMod of R
for W1, W2 being strict Submodule of V st ( for v being Vector of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2 by VECTSP_4:30;