let M be non void finite-degree SubsetFamilyStr; :: thesis: for C, A being Subset of M st A c= C & A is independent holds
ex B being independent Subset of M st
( A c= B & B is_maximal_independent_in C )

let C, A0 be Subset of M; :: thesis: ( A0 c= C & A0 is independent implies ex B being independent Subset of M st
( A0 c= B & B is_maximal_independent_in C ) )

assume that
A1: A0 c= C and
A2: A0 is independent ; :: thesis: ex B being independent Subset of M st
( A0 c= B & B is_maximal_independent_in C )

reconsider AA = A0 as independent Subset of M by A2;
defpred S1[ Nat] means for A being finite Subset of M st A0 c= A & A c= C & A is independent holds
card A <= \$1;
consider n being Nat such that
A3: for A being finite Subset of M st A is independent holds
card A <= n by Def6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
S1[n] by A3;
then A4: ex n being Nat st S1[n] ;
consider n0 being Nat such that
A5: ( S1[n0] & ( for m being Nat st S1[m] holds
n0 <= m ) ) from
now :: thesis: ex A being independent Subset of M st
( A0 c= A & A c= C & not card A < n0 )
0 <= card AA by NAT_1:2;
then A6: (card AA) + 1 >= 0 + 1 by XREAL_1:6;
assume A7: for A being independent Subset of M st A0 c= A & A c= C holds
card A < n0 ; :: thesis: contradiction
then card AA < n0 by A1;
then (card AA) + 1 <= n0 by NAT_1:13;
then consider n being Nat such that
A8: n0 = 1 + n by ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
S1[n]
proof
let A be finite Subset of M; :: thesis: ( A0 c= A & A c= C & A is independent implies card A <= n )
assume that
A9: A0 c= A and
A10: A c= C and
A11: A is independent ; :: thesis: card A <= n
card A < n + 1 by A7, A8, A9, A10, A11;
hence card A <= n by NAT_1:13; :: thesis: verum
end;
then n + 1 <= n by A5, A8;
hence contradiction by NAT_1:13; :: thesis: verum
end;
then consider A being independent Subset of M such that
A12: A0 c= A and
A13: A c= C and
A14: card A >= n0 ;
A15: card A <= n0 by A5, A12, A13;
take A ; :: thesis: ( A0 c= A & A is_maximal_independent_in C )
thus ( A0 c= A & A is independent & A c= C ) by ; :: 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 that
A16: B is independent and
A17: B c= C and
A18: A c= B ; :: thesis: A = B
reconsider B9 = B as independent Subset of M by A16;
card A <= card B9 by ;
then A19: n0 <= card B9 by ;
A0 c= B by ;
then card B9 <= n0 by ;
then card B9 = n0 by ;
hence A = B by ; :: thesis: verum