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

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