let M be finite-degree Matroid; :: thesis: for C being Subset of
for A being independent Subset of st A c= C holds
card A <= Rnk C
let C be Subset of ; :: thesis: for A being independent Subset of st A c= C holds
card A <= Rnk C
let A be independent Subset of ; :: thesis: ( A c= C implies card A <= Rnk C )
assume A c= C ; :: thesis: card A <= Rnk C
then card A in { (card B) where B is independent Subset of : B c= C } ;
then card A c= Rnk C by ZFMISC_1:92;
hence card A <= Rnk C by NAT_1:40; :: thesis: verum