theorem Th12: :: VECTSP_9:12

for GF being Field
for V being VectSp of GF
for W being Subspace 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