theorem Th57: :: ZMODUL02:57

for V being Z_Module
for A being Subset of V st A is linearly-independent holds
not 0. V in A by VECTSP_7:2;