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 A0: ( A0 c= C & A0 is independent ) ; :: thesis: ex B being independent Subset of M st
( A0 c= B & B is_maximal_independent_in C )
then reconsider AA = A0 as independent Subset of M ;
defpred S₁[ 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
A1: for A being finite Subset of M st A is independent holds
card A <= n by Def9;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
S₁[n] by A1;
then A2: ex n being Nat st S₁[n] ;
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);

now

assume B1: for A being independent Subset of M st A0 c= A & A c= C holds
card A < n0 ; :: thesis: contradiction
( card AA < n0 & 0 <= card AA ) by A0, B1, NAT_1:2;
then ( (card AA) + 1 <= n0 & (card AA) + 1 >= 0 + 1 ) by NAT_1:13, XREAL_1:8;
then consider n being Nat such that
B2: n0 = 1 + n by NAT_1:10, XXREAL_0:2;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
S₁[n]

proof

let A be finite Subset of M; :: thesis: ( A0 c= A & A c= C & A is independent implies card A <= n )
assume ( A0 c= A & A c= C & A is independent ) ; :: thesis: card A <= n
then card A < n + 1 by B1, B2;
hence card A <= n by NAT_1:13; :: thesis: verum

end;

then n + 1 <= n by A3, B2;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then consider A being independent Subset of M such that
A4: ( A0 c= A & A c= C & card A >= n0 ) ;
take A ; :: thesis: ( A0 c= A & A is_maximal_independent_in C )
thus ( A0 c= A & 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 A5: ( B is independent & B c= C & A c= B ) ; :: thesis: A = B
then reconsider B' = B as independent Subset of M ;
( A0 c= B & card A <= card B' ) by A4, A5, XBOOLE_1:1, NAT_1:44;
then ( n0 <= card B' & card B' <= n0 & card A <= n0 ) by A3, A4, A5, XXREAL_0:2;
then ( card B' = n0 & card A = n0 ) by A4, XXREAL_0:1;
hence A = B by A5, CARD_FIN:1; :: thesis: verum