:: deftheorem defines is_dependent_on MATROID0:def 14 :
for M being finite-degree Matroid
for e being Element of M
for A being Subset of M holds
( e is_dependent_on A iff Rnk (A \/ {e}) = Rnk A );