let M be finite-degree Matroid; :: thesis:
let C be Subset of M; :: thesis:
set X = { (card A) where A is independent Subset of M : A c= C } ;
let A be independent Subset of M; :: thesis:
consider B being independent Subset of M such that
A1: B c= C and
A2: card B = Rnk C by Th18;

A3: now :: thesis:

let A be independent Subset of M; :: thesis:
assume that
A4: A c= C and
A5: card A = Rnk C ; :: thesis:
thus A is_maximal_independent_in C :: thesis:

proof

thus ( A is independent & A c= C ) by A4; :: according to MATROID0:def 10 :: thesis:
let B be Subset of M; :: thesis:
assume B is independent ; :: thesis:
then reconsider B9 = B as independent Subset of M ;
assume B c= C ; :: thesis:
then card B9 in { (card A) where A is independent Subset of M : A c= C } ;
then A6: card B9 c= Rnk C by ZFMISC_1:74;
assume A7: A c= B ; :: thesis:
then card A c= card B9 by CARD_1:11;
then card A = card B9 by A5, A6;
hence A = B by A7, CARD_2:102; :: thesis:

end;

end;

hereby :: thesis:

assume A8: A is_maximal_independent_in C ; :: thesis:
hence A c= C ; :: thesis:
B is_maximal_independent_in C by A3, A1, A2;
hence card A = Rnk C by A2, A8, Th16; :: thesis:

end;

thus ( A c= C & card A = Rnk C implies A is_maximal_independent_in C ) by A3; :: thesis: