let A be set ; :: according to FINSET_1:def 6,MATROID0:def 6 :: thesis: ( not A in the_family_of (LinearlyIndependentSubsets V) or A is finite )
set M = LinearlyIndependentSubsets V;
assume A in the_family_of (LinearlyIndependentSubsets V) ; :: thesis: A is finite
then A is independent Subset of (LinearlyIndependentSubsets V) by Def2;
then A is linearly-independent Subset of V by Th11;
hence A is finite by VECTSP_9:21; :: thesis: verum