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

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