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:
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 ; :: thesis: verum
end;
end;
hereby :: thesis: ( A c= C & card A = Rnk C implies A is_maximal_independent_in C ) end;
thus ( A c= C & card A = Rnk C implies A is_maximal_independent_in C ) by A3; :: thesis: verum