let M be finite-degree Matroid; :: thesis: for C being finite Subset of M holds

( C is independent iff card C = Rnk C )

let C be finite Subset of M; :: thesis: ( C is independent iff card C = Rnk C )

set X = { (card A) where A is independent Subset of M : A c= C } ;

( A c= C & card A = Rnk C ) by Th18;

hence ( card C = Rnk C implies C is independent ) by CARD_2:102; :: thesis: verum

( C is independent iff card C = Rnk C )

let C be finite Subset of M; :: thesis: ( C is independent iff card C = Rnk C )

set X = { (card A) where A is independent Subset of M : A c= C } ;

hereby :: thesis: ( card C = Rnk C implies C is independent )

ex A being independent Subset of M st assume
C is independent
; :: thesis: card C = Rnk C

then card C in { (card A) where A is independent Subset of M : A c= C } ;

then Segm (card C) c= Segm (Rnk C) by ZFMISC_1:74;

then A1: card C <= Rnk C by NAT_1:39;

Rnk C <= card C by Th20;

hence card C = Rnk C by A1, XXREAL_0:1; :: thesis: verum

end;then card C in { (card A) where A is independent Subset of M : A c= C } ;

then Segm (card C) c= Segm (Rnk C) by ZFMISC_1:74;

then A1: card C <= Rnk C by NAT_1:39;

Rnk C <= card C by Th20;

hence card C = Rnk C by A1, XXREAL_0:1; :: thesis: verum

( A c= C & card A = Rnk C ) by Th18;

hence ( card C = Rnk C implies C is independent ) by CARD_2:102; :: thesis: verum