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 Z0: 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
Z1: ( C c= A & card C = Rnk A ) by ThR1;

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

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

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

end;

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

then consider x being set such that
Z2: ( x in A & x nin C ) by TARSKI:def 3;
reconsider x = x as Element of M by Z2;
A2: ( C \/ {x} c= A & C c= C \/ {x} ) by Z1, Z2, SETWISEO:8;
defpred S₁[ Nat] means ex B being independent Subset of M st
( card B = $1 & B c= C & not B \/ {x} is independent );
Z3: ex n being Nat st S₁[n]

proof

take n = Rnk A; :: thesis: S₁[n]
take C ; :: thesis: ( card C = n & C c= C & not C \/ {x} is independent )
thus ( card C = n & C c= C ) by Z1; :: thesis: not C \/ {x} is independent
A1: C is_maximal_independent_in A by Z1, ThR2;
assume C \/ {x} is independent ; :: thesis: contradiction
then C = C \/ {x} by A1, A2, MAXIMAL;
then {x} c= C by XBOOLE_1:7;
hence contradiction by Z2, ZFMISC_1:37; :: thesis: verum

end;

consider n being Nat such that
Z4: ( S₁[n] & ( for k being Nat st S₁[k] holds
n <= k ) ) from NAT_1:sch 5(Z3);
consider B being independent Subset of M such that
Z5: ( card B = n & B c= C & not B \/ {x} is independent ) by Z4;
B c= A by Z1, Z5, XBOOLE_1:1;
then Z6: ( B \/ {x} c= A & x nin B ) by Z2, Z5, SETWISEO:8;
B \/ {x} is cycle

proof

thus not B \/ {x} is independent by Z5; :: 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};
A5: B \ {e} c= B by XBOOLE_1:36;
assume A3: e in B \/ {x} ; :: thesis: (B \/ {x}) \ {e} is independent

per cases ( e in B or e = x ) by A3, SETWISEO:6;

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

then ( B = (B \ {e}) \/ {e} & e nin B \ {e} ) by ZFMISC_1:64, ZFMISC_1:140;
then B3: n = (card (B \ {e})) + 1 by Z5, CARD_2:54;
assume B2: not (B \/ {x}) \ {e} is independent ; :: thesis: contradiction
(B \/ {x}) \ {e} = (B \ {e}) \/ {x} by B1, Z6, ZFMISC_1:17, XBOOLE_1:87;
then n <= card (B \ {e}) by Z4, A5, B2, Z5, XBOOLE_1:1;
hence contradiction by B3, NAT_1:13; :: thesis: verum

end;

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

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

end;

end;

end;

hence A is independent by Z6, Z0; :: thesis: verum

end;

end;