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

A3: now :: thesis: for A being independent Subset of M st A c= C & card A = Rnk C holds
A is_maximal_independent_in C

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

proof

thus ( A is independent & A c= C ) by A4; :: according to MATROID0:def 10 :: thesis: for B being Subset of M st B is independent & B c= C & A c= B holds
A = B
let B be Subset of M; :: thesis: ( B is independent & B c= C & A c= B implies A = B )
assume B is independent ; :: thesis: ( not B c= C or not A c= B or A = B )
then reconsider B9 = B as independent Subset of M ;
assume B c= C ; :: thesis: ( not A c= B or A = B )
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: A = B
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: verum

end;

end;

hereby :: thesis: ( A c= C & card A = Rnk C implies A is_maximal_independent_in C )

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

end;

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