let M be finite-degree Matroid; :: thesis: for A being Subset of M st ( for B being Subset of M st B c= A holds

not B is cycle ) holds

A is independent

let A be Subset of M; :: thesis: ( ( for B being Subset of M st B c= A holds

not B is cycle ) implies A is independent )

assume A1: for B being Subset of M st B c= A holds

not B is cycle ; :: thesis: A is independent

consider C being independent Subset of M such that

A2: C c= A and

A3: card C = Rnk A by Th18;

not B is cycle ) holds

A is independent

let A be Subset of M; :: thesis: ( ( for B being Subset of M st B c= A holds

not B is cycle ) implies A is independent )

assume A1: for B being Subset of M st B c= A holds

not B is cycle ; :: thesis: A is independent

consider C being independent Subset of M such that

A2: C c= A and

A3: card C = Rnk A by Th18;

per cases
( A c= C or A c/= C )
;

end;

suppose
A c/= C
; :: thesis: A is independent

then consider x being object such that

A4: x in A and

A5: x nin C ;

reconsider x = x as Element of M by A4;

A6: C c= C \/ {x} by ZFMISC_1:137;

defpred S_{1}[ Nat] means ex B being independent Subset of M st

( card B = $1 & B c= C & B \/ {x} is dependent );

A7: C \/ {x} c= A by A2, A4, ZFMISC_1:137;

A8: ex n being Nat st S_{1}[n]

A10: ( S_{1}[n] & ( for k being Nat st S_{1}[k] holds

n <= k ) ) from NAT_1:sch 5(A8);

consider B being independent Subset of M such that

A11: card B = n and

A12: B c= C and

A13: B \/ {x} is dependent by A10;

A14: x nin B by A5, A12;

A15: B \/ {x} is cycle

then B \/ {x} c= A by A4, ZFMISC_1:137;

hence A is independent by A1, A15; :: thesis: verum

end;A4: x in A and

A5: x nin C ;

reconsider x = x as Element of M by A4;

A6: C c= C \/ {x} by ZFMISC_1:137;

defpred S

( card B = $1 & B c= C & B \/ {x} is dependent );

A7: C \/ {x} c= A by A2, A4, ZFMISC_1:137;

A8: ex n being Nat st S

proof

consider n being Nat such that
take n = Rnk A; :: thesis: S_{1}[n]

take C ; :: thesis: ( card C = n & C c= C & C \/ {x} is dependent )

thus ( card C = n & C c= C ) by A3; :: thesis: C \/ {x} is dependent

assume A9: C \/ {x} is independent ; :: thesis: contradiction

C is_maximal_independent_in A by A2, A3, Th19;

then C = C \/ {x} by A7, A6, A9;

then {x} c= C by XBOOLE_1:7;

hence contradiction by A5, ZFMISC_1:31; :: thesis: verum

end;take C ; :: thesis: ( card C = n & C c= C & C \/ {x} is dependent )

thus ( card C = n & C c= C ) by A3; :: thesis: C \/ {x} is dependent

assume A9: C \/ {x} is independent ; :: thesis: contradiction

C is_maximal_independent_in A by A2, A3, Th19;

then C = C \/ {x} by A7, A6, A9;

then {x} c= C by XBOOLE_1:7;

hence contradiction by A5, ZFMISC_1:31; :: thesis: verum

A10: ( S

n <= k ) ) from NAT_1:sch 5(A8);

consider B being independent Subset of M such that

A11: card B = n and

A12: B c= C and

A13: B \/ {x} is dependent by A10;

A14: x nin B by A5, A12;

A15: B \/ {x} is cycle

proof

B c= A
by A2, A12;
thus
B \/ {x} is dependent
by A13; :: according to MATROID0:def 16 :: thesis: for e being Element of M st e in B \/ {x} holds

(B \/ {x}) \ {e} is independent

let e be Element of M; :: thesis: ( e in B \/ {x} implies (B \/ {x}) \ {e} is independent )

set Be = B \ {e};

A16: B \ {e} c= B by XBOOLE_1:36;

assume A17: e in B \/ {x} ; :: thesis: (B \/ {x}) \ {e} is independent

end;(B \/ {x}) \ {e} is independent

let e be Element of M; :: thesis: ( e in B \/ {x} implies (B \/ {x}) \ {e} is independent )

set Be = B \ {e};

A16: B \ {e} c= B by XBOOLE_1:36;

assume A17: e in B \/ {x} ; :: thesis: (B \/ {x}) \ {e} is independent

per cases
( e in B or e = x )
by A17, ZFMISC_1:136;

end;

suppose A18:
e in B
; :: thesis: (B \/ {x}) \ {e} is independent

A19:
e nin B \ {e}
by ZFMISC_1:56;

B = (B \ {e}) \/ {e} by A18, ZFMISC_1:116;

then A20: n = (card (B \ {e})) + 1 by A11, A19, CARD_2:41;

assume A21: (B \/ {x}) \ {e} is dependent ; :: thesis: contradiction

(B \/ {x}) \ {e} = (B \ {e}) \/ {x} by A14, A18, XBOOLE_1:87, ZFMISC_1:11;

then n <= card (B \ {e}) by A10, A12, A16, A21, XBOOLE_1:1;

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

end;B = (B \ {e}) \/ {e} by A18, ZFMISC_1:116;

then A20: n = (card (B \ {e})) + 1 by A11, A19, CARD_2:41;

assume A21: (B \/ {x}) \ {e} is dependent ; :: thesis: contradiction

(B \/ {x}) \ {e} = (B \ {e}) \/ {x} by A14, A18, XBOOLE_1:87, ZFMISC_1:11;

then n <= card (B \ {e}) by A10, A12, A16, A21, XBOOLE_1:1;

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

then B \/ {x} c= A by A4, ZFMISC_1:137;

hence A is independent by A1, A15; :: thesis: verum