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;

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

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

hence A is independent by A2, XBOOLE_0:def 10; :: thesis: verum

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₁[ 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₁[n]

proof

take n = Rnk A; :: thesis: S₁[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;

consider n being Nat such that
A10: ( S₁[n] & ( for k being Nat st S₁[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

proof

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

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

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;

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

hence (B \/ {x}) \ {e} is independent by A14, ZFMISC_1:117; :: thesis: verum

end;

end;

end;

B c= A by A2, A12;
then B \/ {x} c= A by A4, ZFMISC_1:137;
hence A is independent by A1, A15; :: thesis: verum

end;

end;