theorem :: ZMODUL01:18

for R being Ring
for V being LeftMod of R
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
0. V in V1 by VECTSP_4:1;