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