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 } ;

L: now

let A be independent Subset of M; :: thesis: ( A c= C & card A = Rnk C implies A is_maximal_independent_in C )
assume A1: ( A c= C & 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 A1; :: 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 B' = B as independent Subset of M ;
assume B c= C ; :: thesis: ( not A c= B or A = B )
then card B' in { (card A) where A is independent Subset of M : A c= C } ;
then A2: card B' c= Rnk C by ZFMISC_1:92;
assume A3: A c= B ; :: thesis: A = B
then card A c= card B' by CARD_1:27;
then card A = card B' by A1, A2, XBOOLE_0:def 10;
hence A = B by A3, CARD_FIN:1; :: thesis: verum

end;

end;

consider B being independent Subset of M such that
AA: ( B c= C & card B = Rnk C ) by ThR1;
let A be independent Subset of M; :: thesis: ( A is_maximal_independent_in C iff ( A c= C & card A = Rnk C ) )

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

assume A0: A is_maximal_independent_in C ; :: thesis: ( A c= C & card A = Rnk C )
hence A c= C by MAXIMAL; :: thesis: card A = Rnk C
B is_maximal_independent_in C by L, AA;
hence card A = Rnk C by A0, AA, M3; :: thesis: verum

end;

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