theorem :: ZMODUL01:149

for V being Z_Module
for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds
W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Lm16;