let M be finite-degree Matroid; :: thesis: for C being finite Subset of holds Rnk C <= card C
let C be finite Subset of ; :: thesis: Rnk C <= card C
ex A being independent Subset of st
( A c= C & card A = Rnk C ) by Th18;
then Rnk C c= card C by CARD_1:27;
hence Rnk C <= card C by NAT_1:40; :: thesis: verum