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 A0: 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;
A1: A \ {a} is_maximal_independent_in A by A0, C5;
then A \ {a} is independent by MAXIMAL;
then A2: Rnk A = card (A \ {a}) by A1, ThR2;
a in {a} by TARSKI:def 1;
then ( a nin A \ {a} & A = (A \ {a}) \/ {a} ) by XBOOLE_0:def 5, ZFMISC_1:140;
hence (Rnk A) + 1 = card A by A2, CARD_2:54; :: thesis: verum