:: deftheorem Def6 defines finite-degree MATROID0:def 7 :
for M being SubsetFamilyStr holds
( M is finite-degree iff ( M is finite-membered & ex n being Nat st
for A being finite Subset of M st A is independent holds
card A <= n ) );