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 card C c= Rnk C by ZFMISC_1:92;
then ( card C <= Rnk C & Rnk C <= card C ) by ThR3, NAT_1:40;
hence card C = Rnk C by XXREAL_0:1; :: thesis: verum

end;

ex A being independent Subset of M st
( A c= C & card A = Rnk C ) by ThR1;
hence ( card C = Rnk C implies C is independent ) by CARD_FIN:1; :: thesis: verum