for F being Field
for V being VectSp of F
for A being Subset of (LinearlyIndependentSubsets V) holds
( A is independent iff A is linearly-independent Subset of V )