theorem :: ZMODUL01:50

for V being Z_Module
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Submodule of V st V1 = the carrier of W by VECTSP_4:34;