theorem Th13: :: MATROID0:13

for F being Field
for V being VectSp of F
for A being Subset of V st A is linearly-independent holds
for a being Element of V st a nin the carrier of (Lin A) holds
A \/ {a} is linearly-independent