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 )
consider n being Nat such that
A1: for A being finite Subset of M st A is independent holds
card A <= n by Def9;
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 );
A2: ex ne being Nat st S₁[ne]

proof

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

end;

consider n0 being Nat such that
A3: ( S₁[n0] & ( for m being Nat st S₁[m] holds
n0 <= m ) ) from NAT_1:sch 5(A2);
set X = { (card A) where A is independent Subset of M : A c= C } ;

now

let a be set ; :: thesis: ( a in { (card A) where A is independent Subset of M : A c= C } implies a c= n0 )
assume a in { (card A) where A is independent Subset of M : A c= C } ; :: thesis: a c= n0
then consider A being independent Subset of M such that
A4: ( a = card A & A c= C ) ;
card A <= n0 by A3, A4;
hence a c= n0 by A4, NAT_1:40; :: thesis: verum

end;

then A5: Rnk C c= n0 by ZFMISC_1:94;
B1: for k being Nat st S₂[k] holds
k <= n0 by A3;
( card {} = card {} & {} M c= C ) by XBOOLE_1:2;
then B2: ex n being Nat st S₂[n] ;
consider n being Nat such that
B3: ( S₂[n] & ( for m being Nat st S₂[m] holds
m <= n ) ) from NAT_1:sch 6(B1, B2);
consider A being independent Subset of M such that
B4: ( A c= C & n = card A ) by B3;
S₁[n] by B3;
then ( n <= n0 & n0 <= n ) by A3, B3;
then B5: n = n0 by XXREAL_0:1;
then n0 in { (card A) where A is independent Subset of M : A c= C } by B4;
then B6: n0 c= Rnk C by ZFMISC_1:92;
take A ; :: thesis: ( A c= C & card A = Rnk C )
thus ( A c= C & card A = Rnk C ) by B4, B5, B6, A5, XBOOLE_0:def 10; :: thesis: verum