let M be finite-degree Matroid; :: thesis: for C being Subset of M ex A being independent Subset of M st

( A c= C & card A = Rnk C )

let C be Subset of M; :: thesis: ex A being independent Subset of M st

( A c= C & card A = Rnk C )

defpred S_{1}[ Nat] means for A being independent Subset of M st A c= C holds

card A <= $1;

defpred S_{2}[ Nat] means ex A being independent Subset of M st

( A c= C & $1 = card A );

set X = { (card A) where A is independent Subset of M : A c= C } ;

A1: {} M c= C ;

card {} = card {} ;

then A2: ex n being Nat st S_{2}[n]
by A1;

consider n being Nat such that

A3: for A being finite Subset of M st A is independent holds

card A <= n by Def6;

A4: ex ne being Nat st S_{1}[ne]
consider n0 being Nat such that

A5: ( S_{1}[n0] & ( for m being Nat st S_{1}[m] holds

n0 <= m ) ) from NAT_1:sch 5(A4);

A9: for k being Nat st S_{2}[k] holds

k <= n0 by A5;

consider n being Nat such that

A10: ( S_{2}[n] & ( for m being Nat st S_{2}[m] holds

m <= n ) ) from NAT_1:sch 6(A9, A2);

S_{1}[n]
by A10;

then A11: n0 <= n by A5;

consider A being independent Subset of M such that

A12: A c= C and

A13: n = card A by A10;

take A ; :: thesis: ( A c= C & card A = Rnk C )

n <= n0 by A5, A10;

then A14: n = n0 by A11, XXREAL_0:1;

then n0 in { (card A) where A is independent Subset of M : A c= C } by A12, A13;

then n0 c= Rnk C by ZFMISC_1:74;

hence ( A c= C & card A = Rnk C ) by A8, A12, A13, A14; :: thesis: verum

( A c= C & card A = Rnk C )

let C be Subset of M; :: thesis: ex A being independent Subset of M st

( A c= C & card A = Rnk C )

defpred S

card A <= $1;

defpred S

( A c= C & $1 = card A );

set X = { (card A) where A is independent Subset of M : A c= C } ;

A1: {} M c= C ;

card {} = card {} ;

then A2: ex n being Nat st S

consider n being Nat such that

A3: for A being finite Subset of M st A is independent holds

card A <= n by Def6;

A4: ex ne being Nat st S

A5: ( S

n0 <= m ) ) from NAT_1:sch 5(A4);

now :: thesis: for a being set st a in { (card A) where A is independent Subset of M : A c= C } holds

a c= Segm n0

then A8:
Rnk C c= n0
by ZFMISC_1:76;a c= Segm n0

let a be set ; :: thesis: ( a in { (card A) where A is independent Subset of M : A c= C } implies a c= Segm n0 )

assume a in { (card A) where A is independent Subset of M : A c= C } ; :: thesis: a c= Segm n0

then consider A being independent Subset of M such that

A6: a = card A and

A7: A c= C ;

card A <= n0 by A5, A7;

then Segm (card A) c= Segm n0 by NAT_1:39;

hence a c= Segm n0 by A6; :: thesis: verum

end;assume a in { (card A) where A is independent Subset of M : A c= C } ; :: thesis: a c= Segm n0

then consider A being independent Subset of M such that

A6: a = card A and

A7: A c= C ;

card A <= n0 by A5, A7;

then Segm (card A) c= Segm n0 by NAT_1:39;

hence a c= Segm n0 by A6; :: thesis: verum

A9: for k being Nat st S

k <= n0 by A5;

consider n being Nat such that

A10: ( S

m <= n ) ) from NAT_1:sch 6(A9, A2);

S

then A11: n0 <= n by A5;

consider A being independent Subset of M such that

A12: A c= C and

A13: n = card A by A10;

take A ; :: thesis: ( A c= C & card A = Rnk C )

n <= n0 by A5, A10;

then A14: n = n0 by A11, XXREAL_0:1;

then n0 in { (card A) where A is independent Subset of M : A c= C } by A12, A13;

then n0 c= Rnk C by ZFMISC_1:74;

hence ( A c= C & card A = Rnk C ) by A8, A12, A13, A14; :: thesis: verum