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