for M being finite-degree Matroid
for A being Subset of M
for e being Element of M st e is_dependent_on Span A holds
e is_dependent_on A