:: deftheorem Def8 defines LinearlyIndependentSubsets MATROID0:def 9 :
for F being Field
for V being VectSp of F
for b₃ being strict SubsetFamilyStr holds
( b₃ = LinearlyIndependentSubsets V iff ( the carrier of b₃ = the carrier of V & the_family_of b₃ = { A where A is Subset of V : A is linearly-independent } ) );