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;

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

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

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

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

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