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₁[ Nat] means for A being independent Subset of M st A c= C holds
card A <= $1;
defpred S₂[ 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₂[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₁[ne]

proof

take n ; :: thesis: S₁[n]
thus S₁[n] by A3; :: thesis: verum

end;

consider n0 being Nat such that
A5: ( S₁[n0] & ( for m being Nat st S₁[m] holds
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

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;

then A8: Rnk C c= n0 by ZFMISC_1:76;
A9: for k being Nat st S₂[k] holds
k <= n0 by A5;
consider n being Nat such that
A10: ( S₂[n] & ( for m being Nat st S₂[m] holds
m <= n ) ) from NAT_1:sch 6(A9, A2);
S₁[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