theorem Th16: :: ZMODUL03:16

for V being Z_Module
for W being Submodule of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W