let M be finite-degree Matroid; :: thesis: for A being Subset of M st A is cycle holds
(Rnk A) + 1 = card A
let A be Subset of M; :: thesis: ( A is cycle implies (Rnk A) + 1 = card A )
assume A1: A is cycle ; :: thesis: (Rnk A) + 1 = card A
then reconsider A = A as non empty finite Subset of M ;
consider a being Element of A;
A2: A \ {a} is_maximal_independent_in A by A1, Th38;
then A \ {a} is independent by Def10;
then A3: Rnk A = card (A \ {a}) by A2, Th19;
a in {a} by TARSKI:def 1;
then A4: a nin A \ {a} by XBOOLE_0:def 5;
A = (A \ {a}) \/ {a} by ZFMISC_1:140;
hence (Rnk A) + 1 = card A by A3, A4, CARD_2:54; :: thesis: verum