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

let C be finite Subset of M; :: thesis: Rnk C <= card C

ex A being independent Subset of M st

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

then Segm (Rnk C) c= Segm (card C) by CARD_1:11;

hence Rnk C <= card C by NAT_1:39; :: thesis: verum

let C be finite Subset of M; :: thesis: Rnk C <= card C

ex A being independent Subset of M st

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

then Segm (Rnk C) c= Segm (card C) by CARD_1:11;

hence Rnk C <= card C by NAT_1:39; :: thesis: verum