theorem Th30: :: MATROID0:30

for M being finite-degree Matroid
for A being Subset of M
for e being Element of M holds
( e in Span A iff Rnk (A \/ {e}) = Rnk A )