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 that
A1: A is cycle and
A2: e in A ; :: thesis: e is_dependent_on A \ {e}
reconsider Ae = A \ {e} as independent Subset of M by A1, A2;
Ae is_maximal_independent_in A by A1, A2, Th38;
then Rnk A = card Ae by Th19;
hence Rnk ((A \ {e}) \/ {e}) = card Ae by A2, ZFMISC_1:116
.= Rnk (A \ {e}) by Th21 ;
:: according to MATROID0:def 14 :: thesis: verum