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 S_{1}[ 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;

S_{1}[n]
by A3;

then A4: ex n being Nat st S_{1}[n]
;

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);

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 A12, A13; :: 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 A18, NAT_1:43;

then A19: n0 <= card B9 by A14, XXREAL_0:2;

A0 c= B by A12, A18;

then card B9 <= n0 by A5, A17;

then card B9 = n0 by A19, XXREAL_0:1;

hence A = B by A14, A18, A15, CARD_2:102, XXREAL_0:1; :: thesis: verum

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 S

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;

S

then A4: ex n being Nat st S

consider n0 being Nat such that

A5: ( S

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

now :: thesis: ex A being independent Subset of M st

( A0 c= A & A c= C & not card A < n0 )

then consider A being independent Subset of M such that ( 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 A6, NAT_1:10, XXREAL_0:2;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

S_{1}[n]

hence contradiction by NAT_1:13; :: thesis: verum

end;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 A6, NAT_1:10, XXREAL_0:2;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

S

proof

then
n + 1 <= n
by A5, A8;
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;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

hence contradiction by NAT_1:13; :: thesis: verum

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 A12, A13; :: 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 A18, NAT_1:43;

then A19: n0 <= card B9 by A14, XXREAL_0:2;

A0 c= B by A12, A18;

then card B9 <= n0 by A5, A17;

then card B9 = n0 by A19, XXREAL_0:1;

hence A = B by A14, A18, A15, CARD_2:102, XXREAL_0:1; :: thesis: verum