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

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