:: deftheorem Def2 defines independent MATROID0:def 2 :
for M being SubsetFamilyStr
for A being Subset of M holds
( A is independent iff A in the_family_of M );