let M be finite-degree Matroid; :: thesis: for C being Subset of M
for A being independent Subset of M st A c= C holds
card A <= Rnk C
let C be Subset of M; :: thesis: for A being independent Subset of M st A c= C holds
card A <= Rnk C
let A be independent Subset of M; :: 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 M : B c= C } ;
then Segm (card A) c= Segm (Rnk C) by ZFMISC_1:74;
hence card A <= Rnk C by NAT_1:39; :: thesis: verum