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 } ;
hereby :: thesis: ( card C = Rnk C implies C is independent )
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;
ex A being independent Subset of M st
( A c= C & card A = Rnk C ) by Th18;
hence ( card C = Rnk C implies C is independent ) by CARD_2:102; :: thesis: verum