theorem :: ZMODUL01:19

for V being Z_Module
for V1 being Subset of V st V1 is linearly-closed holds
for v being Vector of V st v in V1 holds
- v in V1 by VECTSP_4:2;