:: deftheorem defines Span MATROID0:def 15 :
for M being finite-degree Matroid
for A being Subset of M holds Span A = { e where e is Element of M : e is_dependent_on A } ;