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