:: deftheorem Def12 defines Basis MATROID0:def 13 :
for M being non void finite-degree SubsetFamilyStr
for b₂ being independent Subset of M holds
( b₂ is Basis of M iff b₂ is_maximal_independent_in [#] M );