theorem :: ZMODUL02:56
for V being Z_Module
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent by VECTSP_7:1;