:: deftheorem defines is_maximal_independent_in MATROID0:def 10 :
for M being SubsetFamilyStr
for A, C being Subset of M holds
( A is_maximal_independent_in C iff ( A is independent & A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds
A = B ) ) );