theorem Th21: :: ZMODUL05:32

for V being free finite-rank Z_Module
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent