:: deftheorem Def5 defines finite-membered MATROID0:def 6 :
for M being SubsetFamilyStr holds
( M is finite-membered iff the_family_of M is finite-membered );