let A be set ; :: according to MATROID0:def 5,MATROID0:def 6 :: thesis: ( A in the_family_of (LinearlyIndependentSubsets V) implies 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:25; :: thesis: verum