let M be finite-degree Matroid; :: thesis: 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}
let A be Subset of M; :: thesis: for e being Element of M st A is cycle & e in A holds
e is_dependent_on A \ {e}
let e be Element of M; :: thesis: ( A is cycle & e in A implies e is_dependent_on A \ {e} )
assume Z0: ( A is cycle & e in A ) ; :: thesis: e is_dependent_on A \ {e}
then reconsider Ae = A \ {e} as independent Subset of M by CYCLE;
Ae is_maximal_independent_in A by Z0, C5;
then Rnk A = card Ae by ThR2;
hence Rnk ((A \ {e}) \/ {e}) = card Ae by Z0, ZFMISC_1:140
.= Rnk (A \ {e}) by ThR4 ;
:: according to MATROID0:def 14 :: thesis: verum