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 ;

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; :: thesis: verum

(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 ;

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; :: thesis: verum