theorem :: MATROID0:40

for M being finite-degree Matroid
for A being Subset of M
for e being Element of M st A is cycle & e in A holds
e is_dependent_on A \ {e}